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
--- available.txt 2024-02-12 21:24:05.872721696 -0800 | |
- 1 B2T.fst | |
- 1 Bug3210.fsti | |
- 1 StaticHeaderAPI.fst | |
- 1 titles.fsti | |
- 2 EverParse3d.Actions.BackendFlag.fst | |
- 2 EverParse3d.Actions.BackendFlagValue.fsti | |
- 2 ExtractPulseC.fsti | |
- 2 ExtractSteelC.fsti | |
- 2 LowParseExamplePair.fst |
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
/- REDUNDANT SIMP LEMMAS. | |
Some simp lemmas can be derived from other simp lemmas using `by simp`: -/ | |
-- topology/metric_space/hausdorff_distance.lean | |
#print metric.Hausdorff_dist_closure /- is redundant: by simp [metric.Hausdorff_dist_closure₁, metric.Hausdorff_dist_closure₂] -/ | |
#print metric.Hausdorff_dist_self_closure /- is redundant: by simp [metric.Hausdorff_dist_self_zero, metric.Hausdorff_dist_closure₂] -/ | |
#print emetric.Hausdorff_edist_self_closure /- is redundant: by simp [emetric.Hausdorff_edist_self, emetric.Hausdorff_edist_closure₂] -/ | |
#print emetric.Hausdorff_edist_closure /- is redundant: by simp [emetric.Hausdorff_edist_closure₁, emetric.Hausdorff_edist_closure₂] -/ | |
-- topology/category/Top/opens.lean |
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
fof(ccanonically__ordered__comm__semiring_o_to__comm__semiring, axiom, | |
(![X_ga_n2]: (p(ccanonically__ordered__comm__semiring(X_ga_n2)) => p(ccomm__semiring(X_ga_n2))))). | |
fof(ccanonically__ordered__comm__semiring_o_to__zero__ne__one__class, axiom, | |
(![X_ga_n3]: (p(ccanonically__ordered__comm__semiring(X_ga_n3)) => p(czero__ne__one__class(X_ga_n3))))). | |
fof(ccomm__group_o_to__comm__monoid, axiom, (![X_ga_n5]: (p(ccomm__group(X_ga_n5)) => p(ccomm__monoid(X_ga_n5))))). | |
fof(ccomm__group_o_to__group, axiom, (![X_ga_n6]: (p(ccomm__group(X_ga_n6)) => p(cgroup(X_ga_n6))))). |
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
1 #NS 0 u | |
2 #NS 0 eq | |
3 #NS 0 α | |
1 #UP 1 | |
0 #ES 1 | |
4 #NS 0 a | |
1 #EV 0 | |
2 #EV 1 | |
3 #ES 0 | |
4 #EP #BD 4 2 3 |
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) |
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
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 α |
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
-- 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.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) |
NewerOlder