gebner

--- 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

gebner

/- 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

gebner

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))))).

gebner

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

gebner

/-   syntax   -/

structure position :=
(line : ℕ) (column : ℕ)

structure range :=
(left : position) (right : position)

structure location :=
(file : string) (range : range)

gebner

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)

-/

gebner

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

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 :=

gebner

-- 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

gebner

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)