lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
This is what I have so far, mainly typo fixes and minor clarifications and a couple new docstrings. I also noticed that the interface of `elimMVar` could be simplified. I...
This adds two combinators for working directly with uniqueness: ```lean @[extern] def withSquashIsShared (a : α) (f : α → Squash Bool → β) : β def withIsShared (a :...
This makes the type a bit less error-prone, by not exposing the constructor or eliminator for the type (which is almost certainly an error given that elements of this type...
This makes the following changes: 1. It adds a `src/Lean/Compiler/IR/LLVMBindings.lean` with the C API bindings required for the LLVM backend 2. It adds a stub `src/Lean/Compiler/IR/EmitLLVM.cpp`, to import `LLVMBindings` and...
### 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). *...
```lean example (h : P) : P ∨ Q := by apply .inl -- type mismatch -- Or.inl -- has type -- ?m.23 → ?m.23 ∨ ?m.24 : Prop --...
this works: ```lean example (h : P ∨ Q) : True := by cases h case _ hpq => trivial case _ hpr => trivial ``` but this doesn't: ```lean...
easy: ```lean example : 1 + 1 = 2 := by sim --^ textDocument/completion ``` harder: ```lean example : 1 + 1 = 2 := by skip --^ textDocument/completion done...
```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`)...
### 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)....
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover