Leonardo de Moura
Leonardo de Moura
@kha @gebner: we have been talking about the parser refactoring for a few months. @david-christiansen has many ideas and suggestions. I'm open this RFC to record his ideas and collect...
`tactic.copy_attribute` copies local attributes as permanent ones. To fix it, we need an API for checking whether an attribute is local or not. This bug is affecting `transport_multiplicative_to_additive`. See PR...
We currently use type class resolution to implement coercion resolution. The type classes are defined in the following file https://github.com/leanprover/lean/blob/master/library/init/coe.lean The resolution process is described in Section 10.6 at https://leanprover.github.io/theorem_proving_in_lean/...
@gebner Commit bcf44f7 introduced a bug in the equation compiler. The failure happens when we are proving equational lemmas. Here is a minimal example: ```lean inductive type | bool :...
We currently use trace messages to diagnose problems. Examples: why two terms didn't unify, why the simplifier didn't do what we wanted, etc. We have different trace message classes, and...
The `case` tactic is super nice for structuring proofs. However, if it doesn't solve the goal, the error position is very inconvenient. Here is an example: ```lean example (a b...
The equation compiler currently supports the following compilation strategies - `brec_on` (aka course of values recursion) - `well_founded` recursion - `unbounded` recursion for meta definitions - Non recursive However, none...
During the ICERM after-party hackton, @digama0 suggested we add helper abbreviations such as ```lean abbrev MVarId.getType (mvarId : MVarId) : MetaM Expr ``` They are great for discoverability when using...
Lean 3 can run on the web browser. The code is compiled into javascript using emscripten https://emscripten.org/ We need this feature in Lean 4 to be able to have interactive...
The goal is to have something like Rust Cargo. https://github.com/rust-lang/cargo It should be implemented in Lean. Core developers will help with missing APIs.