Search results

"unused variable" warning for variable used by typclass inference

bugSomething isn't workingSomething isn't working

Status: Open.

#13269 In leanprover/lean4;

· andres-erbsen opened on Apr 3, 2026

named local syntax can only have two name components

bugSomething isn't workingSomething isn't working

Status: Open.

#13268 In leanprover/lean4;

· Rob23oba opened on Apr 3, 2026

(new do elaborator) go to definition on do elements only shows generic documentation for bind

bugSomething isn't workingSomething isn't working

Status: Open.

#13267 In leanprover/lean4;

· Rob23oba opened on Apr 3, 2026

kernel error in simple grind proof

bugSomething isn't workingSomething isn't working

Status: Open.

#13265 In leanprover/lean4;

· b-mehta opened on Apr 3, 2026

split fails with let declarations

bugSomething isn't workingSomething isn't working

Status: Open.

#13263 In leanprover/lean4;

· Rob23oba opened on Apr 2, 2026

Inconsistent name resolution with generalized field notation in opened namespaces

bugSomething isn't workingSomething isn't working

Status: Open.

#13261 In leanprover/lean4;

· fiforeach opened on Apr 2, 2026

RFC: Don't shake deprecated modules

RFCRequest for commentsRequest for comments

Status: Open.

#13236 In leanprover/lean4;

· SnirBroshi opened on Apr 1, 2026

RFC: lake should give a warning if a project is called test

RFCRequest for commentsRequest for comments

Status: Open.

#13227 In leanprover/lean4;

· riccardobrasca opened on Apr 1, 2026

RFC: Field attributes

RFCRequest for commentsRequest for comments

Status: Open.

#13221 In leanprover/lean4;

· SrGaabriel opened on Mar 31, 2026

RFC: Inconsistency between interfaces for Nat.gcd/Nat.lcm and Int.gcd/Int.lcm

RFCRequest for commentsRequest for comments

Status: Open.

#13218 In leanprover/lean4;

· Applimu opened on Mar 31, 2026

try? errors because simp errors

bugSomething isn't workingSomething isn't working

Status: Open.

#13216 In leanprover/lean4;

· MoritzBeroRoos opened on Mar 31, 2026

Bug: grind linarith crashes in the presence of conflicting hAdd instances

bugSomething isn't workingSomething isn't working

Status: Open.

#13214 In leanprover/lean4;

· sonmarcho opened on Mar 31, 2026