Search results

Type error in simp

bugSomething isn't workingSomething isn't working

Status: Open.

#12398 In leanprover/lean4;

· BrunoDutertre opened on Feb 9, 2026

Overlapping tactic syntax hides error messages

bugSomething isn't workingSomething isn't working

Status: Open.

#12394 In leanprover/lean4;

· Vierkantor opened on Feb 9, 2026

@[grind] cannot deal with eta-expanded terms

bugSomething isn't workingSomething isn't working

Status: Open.

#12390 In leanprover/lean4;

· JovanGerb opened on Feb 9, 2026

<code>cbv</code> does not reduce a recursor

bugSomething isn't workingSomething isn't working

Status: Open.

#12386 In leanprover/lean4;

· wkrozowski opened on Feb 9, 2026

Typeclass inference fails if argument is a <code>match</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#12381 In leanprover/lean4;

· btj-h opened on Feb 8, 2026

Unnecessarily verbose error message when main is undefined

Status: Open.

#12378 In leanprover/lean4;

· nielsvoss opened on Feb 8, 2026

<code>unknown free variable</code> in the info-view with <code>rcases</code> patterns

bugSomething isn't workingSomething isn't working

Status: Open.

#12369 In leanprover/lean4;

· SnirBroshi opened on Feb 6, 2026

Error when using public structure with private field of private type from a different module

bugSomething isn't workingSomething isn't working

Status: Open.

#12337 In leanprover/lean4;

· georgerennie opened on Feb 5, 2026

Undefined behavior in lean::MurmurHash64A for unaligned

bugSomething isn't workingSomething isn't working

Status: Open.

#12317 In leanprover/lean4;

· eric-wieser opened on Feb 5, 2026

Over eager simplification of Array.drop

bugSomething isn't workingSomething isn't working

Status: Open.

#12299 In leanprover/lean4;

· cmlsharp opened on Feb 4, 2026

Bad rendering of "apply suggestions" on hover

bugSomething isn't workingSomething isn't working

Status: Open.

#12292 In leanprover/lean4;

· ejgallego opened on Feb 3, 2026

<code>mvcgen</code> fails to transform matcher when <code>let</code> values are used under a dependent <code>match</code>

bugSomething isn't workingSomething isn't working

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the time

Status: Open.

#12275 In leanprover/lean4;

· datokrat opened on Feb 2, 2026