lean4

lean4 copied to clipboard

### Description When autocompleting a namespace (e,g, `Lean.PrettyPrinter`) on a non-initial part (e.g., `PrettyPrinter`), Lean will insert the full name of the namespace at that segment (e.g., `Lean.Lean.PrettyPrinter`) rather than...

tydeu

`rintro` error message is in the wrong place

1

### 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...

TwoFX

The `Meta.check` function is incomplete, in particular for projections: ``` private partial def checkAux (e : Expr) : MetaM Unit := do check e |>.run where check (e : Expr)...

nomeata

"failed to generate equational theorem" when matching on not only recursive call

5

This could be a duplicate of #3219 or #2962. Still reporting it separately, so when a fix is applied each example can be checked and closed separately, and nothing falls...

nomeata

### 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...

TwoFX

### 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...

jjdishere

Slow elaboration of `List Nat` literals

3

### Description Long lists of natural number literals can take a long time to elaborate. ### Context Reported by @dwrensha [on the Lean Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/slow.20elaboration.20of.20.60List.20Nat.60.20literal/near/476530139). ### Steps to Reproduce Given the...

kmill

### Description Given universe level `max u v w`, it gets normalized as `max (max u v) w`. ### Steps to Reproduce In the following, the `structure` command derives the...

kmill

### 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...

JLimperg

### 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...

fpvandoorn