36 lines
1.7 KiB
Text
36 lines
1.7 KiB
Text
A list of bugs and/or unintuitive behavior in Lean 2:
|
|
|
|
- When using the "have" or "assert" tactic, no coercion is applied to the type. So you have to write for example
|
|
`have g : Group.carrier G, from _,`
|
|
instead of
|
|
`have g : G, from _,`
|
|
|
|
- coercions are still displayed by the pretty printer
|
|
|
|
- When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`)
|
|
|
|
- A file named "module.hlean" cannot be imported using `import .module` because `module` is a keyword (but it can be imported using `import ..foo.module`)
|
|
|
|
Issues which are not bugs, but still good to know
|
|
|
|
- once you start tactic mode, you cannot specify universe levels anymore
|
|
|
|
- esimp is slow, and runs out of memory easily. It is good behavior to split up definitions. So instead of
|
|
```
|
|
equiv.MK (* big function *)
|
|
(* big inverse *)
|
|
(* long proof *)
|
|
(* long proof *)
|
|
```
|
|
first write the functions f and g and then write
|
|
```
|
|
equiv.MK f
|
|
g
|
|
abstract (* long proof *) end
|
|
abstract (* long proof *) end
|
|
```
|
|
this has the additional advantage that if f and/or g are defined using induction, they will only reduce if they are applied to arguments for which they actually reduce (assuming they have the correct [unfold n] flag.
|
|
|
|
- unfold [foo] also does various (sometimes unwanted) reductions (as if you called esimp)
|
|
|
|
- The Emacs flycheck mode has a hard time with nonrelative paths to files in the same directory. This means that for importing files from the Lean 2 HoTT library use absolute paths (e.g. `import algebra.group`) and for importing files in the Spectral repository use relative paths (e.g. for a file in the `homotopy` folder use `import ..algebra.subgroup`)
|