Leonardo de Moura
Leonardo de Moura
When `pp.beta` is set to `true`, the pretty-printer (delaborator) should apply beta reduction. Lean 3 implements this feature, but we had *not* implemented it yet in Lean 4.
The following example ```lean import Lean open Lean.Meta #check ({} : Context) ``` produces ```lean { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox :=...
We have only one reduction strategy when checking definitional equality in the kernel. It uses the "lazy unfolding" and it is suboptimal for many applications. Examples: - Any application that...
Linters
We need many different linters. - Style violations. - Common mistakes. - Bad idioms. - Potential performance problems. The different linters can be developed independently of each other, and they...
Andrew Kent pointed out we were using the `!` for both macros and functions that may panic at runtime. We decided to use it only for functions that panic, and...
The notation `"..."` would now behave like `s!"..."`, and we would have a notation for raw strings.
Example: ```lean inductive Cover : (x y z : List α) -> Type u | done : Cover [] [] [] | left : Cover x y z -> Cover...
The function `IndPredBelow.mkBelow` fails to generate `brecOn` for the following inductive predicate. ```lean set_option trace.Meta.IndPredBelow true in inductive TransClosure (r : α → α → Prop) : α → α...
`simp` currently preprocess theorems marked with `[simp]`, and may create auxiliary theorems. For example, it will use `propext` for converting `a b` into `a = b`. Mathlib 4 currently has...
- Add support for reserved declaration names. We use them for theorems generated on demand. - Equation theorems are not private declarations anymore. - Generate equation theorems on demand when...