gebner
/ gist:5ad2dd58e59655f0a27f
Created
May 31, 2015 15:11
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
| these derivations will be built: | |
| /nix/store/i7cw1vwyl0z8z5nw6r5zgngcgdcd5a7g-openjdk-8u40b27.drv | |
| building path(s) ‘/nix/store/r5l8xfa19qnnd55i24wqb11byiqqy69i-openjdk-8u40b27’, ‘/nix/store/wl290af9v112flv2qghgmapdp6cfk7a5-openjdk-8u40b27-jre’ | |
| unpacking sources | |
| unpacking source archive /nix/store/ww0r6ynfvys9zz59m2jq8krildiihrlh-jdk8u40-b27.tar.gz | |
| unpacking source archive /nix/store/3q6n1zzjqk68bip7frz7d605m3il1c27-jdk8u40-b27.tar.gz | |
| unpacking source archive /nix/store/83km313n799ki3sc9g09ildhdpsnh01s-jdk8u40-b27.tar.gz | |
| unpacking source archive /nix/store/piig7c9aaj3bhkczxld6bsx8azychgk8-jdk8u40-b27.tar.gz | |
| unpacking source archive /nix/store/1pqabhkydpswqzflqc9kbbl7cvfz3ipf-jdk8u40-b27.tar.gz | |
| unpacking source archive /nix/store/xybxivlkvpmx8q75ahp60nb0mgwngncy-jdk8u40-b27.tar.gz |
gebner
/ verit-bomb.smt
Created
July 20, 2015 06:03
toDeep SMT-LIB export for ./testing/TSTP/prover9/GRP/GRP098-1/Prover9---1109a.UNS-Ref.s.out
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
| (set-logic QF_UF) | |
| (declare-sort S 0) | |
| (declare-fun b4 () S) | |
| (declare-fun a1 () S) | |
| (declare-fun b2 () S) | |
| (declare-fun v3$ () S) | |
| (declare-fun v10$ () S) | |
| (declare-fun a2 () S) | |
| (declare-fun divide (S S ) S) | |
| (declare-fun c3 () S) |
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
| set(quiet). | |
| clear(auto_denials). | |
| formulas(sos). | |
| -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f1,f6(f4,f0(f1,f9)))) | -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))) | =(f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))). | |
| f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f1,f6(f4,f0(f1,f9)))). | |
| f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f6(f4,f0(f1,f9)),f6(f4,f0(f1,f9)))). | |
| f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))). | |
| -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))) | -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f6(f4,f0(f1,f9)),f6(f4,f0(f1,f9)))) | =(f0(f9,f0(f1,f6(f4,f0(f1,f9)))),f6(f4,f0(f1,f9))). | |
| -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f1,f6(f4,f0(f1,f9))))) | -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))) | =(f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))). | |
| f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f1,f6(f4,f0(f1,f9))))). |
gebner
/ deep-recursion.lean
Created
January 30, 2017 10:13
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 gapt | |
| open tactic expr | |
| namespace lk | |
| lemma LogicalAxiom {a} (main1 : a) (main2 : ¬a) : false := main2 main1 | |
| lemma BottomAxiom (main : false) : false := main | |
| lemma TopAxiom (main : ¬true) : false := main ⟨⟩ | |
| lemma ReflexivityAxiom {α : Type} {a : α} (main : a ≠ a) : false := main (eq.refl a) |
gebner
/ list_rev.lean
Created
February 13, 2017 16:20
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.stream | |
| open list | |
| def list_rev_bench (size : ℕ) : ℕ := | |
| head $ stream.iterate reverse (iota (10*size)) size | |
| vm_eval let size := 1200 in | |
| timeit ("list_rev_bench " ++ size^.to_string ++ ":") (list_rev_bench size) |
gebner
/ segfault2.lean
Created
February 15, 2017 12:50
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
| -- standard setup | |
| lemma they_are_isomorphic (x : false) : ℕ = (ℕ × ℕ) := | |
| by contradiction | |
| def repack (x : unit → false) (y : ℕ) : ℕ × ℕ := | |
| cast (they_are_isomorphic (x ())) y | |
| def proj_nat (x : unit → false) : ℕ → ℕ := | |
| prod.fst ∘ repack x |
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.hash_map | |
| universes u v w | |
| def lens (α β : Type u) := | |
| ∀ (f : Type u → Type w) [functor f], (β → f β) → (α → f α) | |
| def lens.compose {α β δ : Type u} (l₂ : lens α β) (l₁ : lens β δ): lens α δ := | |
| λ f h, @l₂ f h ∘ @l₁ f h | |
| instance : applicative id := |
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.buffer | |
| universes u v | |
| inductive parse_result (α : Type u) | |
| | done (pos : ℕ) (result : α) : parse_result | |
| | fail (pos : ℕ) (expected : list (unit → string)) : parse_result | |
| def parser (α : Type u) := | |
| ∀ (input : char_buffer) (start : ℕ), parse_result α |
gebner
/ coindpred.lean
Last active
May 16, 2017 15:10
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.stream | |
| universes u | |
| /- | |
| coinductive alternating : stream bool → Prop | |
| | f : ∀ s, alternating (ff :: s) → alternating (tt :: ff :: s) | |
| | t : ∀ s, alternating (tt :: s) → alternating (ff :: tt :: s) | |
| -/ |
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
| /- syntax -/ | |
| structure position := | |
| (line : ℕ) (column : ℕ) | |
| structure range := | |
| (left : position) (right : position) | |
| structure location := | |
| (file : string) (range : range) |
OlderNewer