Floris van Doorn
Floris van Doorn
Some things which could be nicer about the file of monoids and groups: * [x] Split up the file `Monoids_and_Groups.v` in two or more parts * [x] Define kernels and...
In the commit https://github.com/leanprover/lean2/commit/d38979f783416c3b2a3a608640b8cf1e243770d6 'unreachable' code was reached when elaborating this theorem on some machines: https://github.com/leanprover/lean2/blob/d38979f783416c3b2a3a608640b8cf1e243770d6/hott/types/trunc.hlean#L299 I worked around it by rewriting the proof in the two commits after that....
... if the projection notation can also be interpreted as a single name: ```lean def foo := none.get_or_else.{3 4 5} 1 -- succeeds def bar := (none).get_or_else.{3 4 5} 1...
... if a component of a name contains a period. See maxhaslbeck/proving-contest-backends#27
See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/options.20in.20user.20attributes
### Description In the code snippet below, the second `congr` raises an error, presumably because I'm already "inside" an `funext`. In my actual case I wanted to rewrite inside a...
A tactic ``` `[ t ]``` used in a tactic definition `my_tac` at line `L` column `C` in file `X` that is used in file `Y` produces output (a server...
The following fails ```lean -- set_option trace.elaborator_detail true def my_eq {A : Type*} (a b : A) : Prop := true lemma id_map_is_right_neutral {A : Type} (map : A ->...
### Description Printing of notation doesn't seem to work when the declaration used `@`. ### Steps to Reproduce ```lean -- uncomment one notation A `⁻` := set.compl A -- prints...
* From the sphere eversion project --- [](https://gitpod.io/from-referrer/)