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). *...
### Description In the widget view, if you hover over the `i` in `∃ i, ...` it doesn't show the type of `i`, but the type of the lambda that...
### 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). *...
### 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). *...
### 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). *...
Hi I've collected some thoughts on how to proceed with making a good code completions / actions interface for Lean: # Scope This RFC intends to cover an API for...
### 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 (P : Nat → Prop) (a) (h : ∃ n, a = n + 1 ∧ P n) : ∃ n, P n := by let ⟨n', e,...
`simp` currently preprocess theorems marked with `[simp]`, and may create auxiliary theorems. For example, it will use `propext` for converting `a b` into `a = b`. Mathlib 4 currently has...
### 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