Gabriel Ebner
Gabriel Ebner
**Checklist** - [x] I searched the `:help` documentation using `/` for helpful information - [x] I have read the [frequently asked questions](https://github.com/Jelmerro/Vieb/blob/master/FAQ.md) - [x] I did not find any similar...
VM error
The following fails with `error: vm check failed: i < 2 (possibly due to incorrect axioms, or sorry)`: ```lean def join (sep : string) : list string → string |...
This PR contains a number of improvements to trace messages, most notably collapsible trace nodes can now have a message. Before (neovim screenshot): ``` [Meta.synthInstance] ▼ [Meta.synthInstance] main goal R...
```lean example [Inhabited Empty] : α := (default : Empty).rec --^ term goal (instance missing) example [Inhabited α] : α := default --^ term goal (instance shown) example [Inhabited α]...
Lean only has a single concurrency primitive right now, `Task`, which is very nice when it fits your use case (and also hard to misuse) but you can't easily use...
In Lean 3 we had `by have : stmt := proof; exact term` which added `stmt` to the local context *without leaving any trace behind*. In Lean 4 `have` always...
```lean import Lean open Lean @[defaultInstance] instance : MonadQuotation Elab.TermElabM := inferInstance syntax "👉" (ident "_") : term #eval `(👉 $_) ``` The last underscore has type ``TSyntax `ident``, which...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
From #348: Lean 4 defines `max` and `min` in the prelude, while Lean 3 (as of https://github.com/leanprover-community/lean/pull/609) defines them differently as part of `linear_order`. We will need to figure out...