lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
### 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). *...
Gonna use this issue to collect a few unexpected results I've encountered * searching for `smap` or `SMap` does not find the actual type
### 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). *...
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,...
I haven't quite figured out the MWE yet. Possibly a vscode-lean4 bug. There seem to be certain files for me where vscode and Lean will stop talking to each other....
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...
```lean example [Monad m] [LawfulMonad m] (h : a) : foo a := sorry --^ $/lean/plainTermGoal ``` ``` PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:370:17: unknown metavariable backtrace: libleanshared.so(+0x30f516c)[0x7f741be3516c] libleanshared.so(lean_panic_fn+0xc4)[0x7f741be354d4] libleanshared.so(l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at___private_Lean_Meta_PPGoal_0__Lean_Meta_ToHide_findDeps___spec__10+0x90c)[0x7f7419fa66cc] libleanshared.so(l___private_Lean_Meta_PPGoal_0__Lean_Meta_ToHide_findDeps+0x7d4)[0x7f7419faa874] libleanshared.so(l_Lean_Meta_ToHide_hasInaccessibleNameDep+0x115)[0x7f7419fadfe5]...
Example: ```lean inductive Cover : (x y z : List α) -> Type u | done : Cover [] [] [] | left : Cover x y z -> Cover...
Lean 3: ```lean @[elab_as_eliminator] theorem eq.subst' {α} {motive : α → Prop} {a b : α} : a = b → motive a → motive b := eq.subst example {α}...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover