Gabriel Ebner
Gabriel Ebner
On my desktop, every additional dependency seems to add 250ms to the startup time (it's almost twice as much on my laptop). For example calling `lake env true` on [doc-gen4](https://github.com/leanprover/doc-gen4)...
When you have a file with lots of errors, the output of `lake build` ends in the following: ``` ⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val error: external command...
As reported on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20function.20coercion.20inference/near/303901188). This used to be supported in Lean 3 (community edition), and is used pretty heavily in mathlib: ```lean structure Equiv (α : Sort _) (β :...
```lean #eval show Nat from False.rec (by decide) ``` - In the server the file crashes. - On the command line it prints `unreachable code` (original report produced `incomplete case`)...
Most syntax coercions are declared like this: ```lean instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where coe id := mkNode _ #[id, mkNullNode #[]] ``` Since we're inlining coercions during elaboration,...
The workspace symbol search (`ctrl-p #` in vscode) returns all kinds of internal definitions. Example queries: - `_sunfold` returns smart unfolding lemmas - `_unsafe_rec` returns helper definitions used to compile...
In short, the question is whether the following cast is safe: ```lean opaque Foo : Type := Bool unsafe def foo : Foo := unsafeCast "123" ``` This pattern is...
We want to use pointer equality as a performance optimization. For example, as a first check in `DecidableEq` instances: if the two arguments are pointer-equal, then we can immediately return...
https://github.com/leanprover-community/lean3port/compare/ported