lean4

lean4 copied to clipboard

I would expect this to work ``` example (x : Fin 3) : x ≠ x + 1 := by omega abbrev Foo := Fin 3 /-- error: omega could...

nomeata

clear does not work in `conv` mode

3

``` example (h : z = 42) (x y : Nat) : y + 0 = y := by conv => lhs tactic => clear h -- tactic 'clear' failed,...

bollu

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

eric-wieser

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...

hargoniX

Git conflict experiment

1

This is an experiment to have git conflict syntax be processed like comments. The option `parser.git.useIncoming` controls whether to use the incoming or current versions. @jcommelin @adomani

kmill

Metavariable instantiation seems to slow down non-linearly in the size of the proof

4

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [ ] Reduce...

alexkeizer

feat: improved `calc` error messages

3

Makes the error messages report on RHSs and LHSs that do not match the expected values when the relations are defeq. If the relations are not defeq, the error message...

kmill

feat: simp local confluence testing

2

This adds @nomeata's simp local confluence testing tool in `tests/simplc`, and sets up whitelists to run this on the core Lean library. The README contains instructions for running this is...

kim-em

feat: `debug.proofAsSorry`

2

An experimental variant of `debug.byAsSorry`

Kha

Deprecate and remove `inductive` ... `:=`

12

### Description Today, Lean accepts all of the following: ``` inductive DogSound | woof | grr ``` ``` inductive DogSound := | woof | grr ``` ``` inductive DogSound where...

david-christiansen