Search results

"This pattern contains metavariables" when using structure constructor and omitting a proof parameter

bugSomething isn't workingSomething isn't working

Status: Open.

#11885 In leanprover/lean4;

· kmill opened on Jan 3, 2026

<code>conv in</code> can unexpectedly fail with <code>unknown metavariable</code> error

bugSomething isn't workingSomething isn't working

Status: Open.

#11877 In leanprover/lean4;

· vlad902 opened on Jan 2, 2026

grind/grobner doesn't finish a proof for a medium-sized problem within reasonable limit

low priority

performanceA performance problem related issue or PRA performance problem related issue or PR

Status: Open.

#11861 In leanprover/lean4;

· wwylele opened on Jan 1, 2026

Inductive type declaration UX bug involving a <code>where</code> typo

bugSomething isn't workingSomething isn't working

Status: Open.

#11853 In leanprover/lean4;

· Chris-F5 opened on Dec 31, 2025

<code>sizeOf</code> generation failure on higher-order nested types

bugSomething isn't workingSomething isn't working

Status: Open.

#11828 In leanprover/lean4;

· arthur-adjedj opened on Dec 29, 2025

Compiler crashes on modules that import both a precompiled library and <code>Lake.CLI</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#11827 In leanprover/lean4;

· zqy1018 opened on Dec 29, 2025

"The recommended spelling of ¬ in identifiers is not" is wrong

bugSomething isn't workingSomething isn't working

Status: Open.

#11826 In leanprover/lean4;

· safinaskar opened on Dec 29, 2025

<code>declare_syntax_cat</code> in private section causes "unknown constant" on import

bugSomething isn't workingSomething isn't working

Status: Open.

#11823 In leanprover/lean4;

· datokrat opened on Dec 29, 2025

RFC: improving performance of <code>deriving Hashable</code> on single-field structures

RFCRequest for commentsRequest for comments

Status: Open.

#11818 In leanprover/lean4;

· math-fehr opened on Dec 28, 2025

Metavariable introduced in pattern match

bugSomething isn't workingSomething isn't working

Status: Open.

#11817 In leanprover/lean4;

· math-fehr opened on Dec 28, 2025

Race condition in lean4 stage2+ builds

bugSomething isn't workingSomething isn't working

Status: Open.

#11808 In leanprover/lean4;

· NicolasRouquette opened on Dec 27, 2025

Add getElem?_mergeWith lemma for TreeMap/DTreeMap

Status: Open.

#11807 In leanprover/lean4;

· alok opened on Dec 27, 2025