This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Aesop | |
variable [LE α] [DecidableRel ((· ≤ ·) : α → α → Prop)] | |
@[aesop safe constructors] | |
inductive Sorted : List α → Prop where | |
| nil : Sorted [] | |
| single : Sorted [x] | |
| cons_cons : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where | |
trans : r a b → s b c → t a c | |
export Trans (trans) | |
instance (r : α → γ → Prop) : Trans Eq r r where | |
trans heq h' := heq ▸ h' | |
instance (r : α → β → Prop) : Trans r Eq r where | |
trans h' heq := heq ▸ h' |
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
namespace nqueens | |
open nat | |
class lt (n : out_param ℕ) (m : ℕ) | |
instance succ_lt_succ_of_lt (n m) [lt n m] : lt (succ n) (succ m) := by constructor | |
instance zero_lt_succ (m) : lt 0 (succ m) := by constructor | |
class ne (n m : ℕ) | |
instance ne_of_lt (n m) [lt n m] : ne n m := by constructor | |
instance ne_of_gt (n m) [lt m n] : ne n m := by constructor |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import data.set.finite | |
-- we don't need no infinite sets here | |
open finset | |
open function | |
-- `fin n` is the type of the first `n` natural numbers | |
theorem pigeonhole (n m : ℕ) (f : fin n → fin m) : n > m → ¬(injective f) := | |
assume : n > m, | |
-- proof of negation: show contradiction |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
section | |
universe u | |
parameters (α β : Type u) (op : α → β → Prop) | |
structure chained_op_val := | |
(left : α) | |
(right : β) | |
(val : Prop) | |
instance coe_chained_op_val : has_coe chained_op_val Prop := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import socket, json | |
import random, pprint | |
import sys | |
import math | |
import re | |
class arith_list(list): | |
def __add__(self, other): | |
return arith_list([x + y for x, y in zip(self, other)]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def heap_rec(f): | |
stack = [f] | |
result = None | |
while stack: | |
try: | |
stack.append(stack[-1].send(result)) | |
result = None | |
except StopIteration as ex: | |
result = ex.value | |
stack.pop() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// ==UserScript== | |
// @name DomJudge IP | |
// @namespace http://nullrich.de | |
// @include http://domjudge.iti.uni-karlsruhe.de/*/submissions.php* | |
// @require https://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js | |
// ==/UserScript== | |
function deserialize(name, def) { | |
return eval(GM_getValue(name, (def || '({})'))); | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--- a/src/handlers.c | |
+++ b/src/handlers.c | |
@@ -717,6 +717,7 @@ int handle_window_type(void *data, xcb_connection_t *conn, uint8_t state, xcb_wi | |
*/ | |
static bool handle_normal_hints(void *data, xcb_connection_t *conn, uint8_t state, xcb_window_t window, | |
xcb_atom_t name, xcb_get_property_reply_t *reply) { | |
+ return true; | |
Con *con = con_by_window_id(window); | |
if (con == NULL) { | |
DLOG("Received WM_NORMAL_HINTS for unknown client\n"); |
NewerOlder