Search results

grind: cannot run cases on type that is a class field

bugSomething isn't workingSomething isn't working

Status: Open.

#13809 In leanprover/lean4;

· robin-carlier opened on May 21, 2026

Implement grind_propagator for downstream / mathlib use

Status: Open.

#13805 In leanprover/lean4;

· kim-em opened on May 20, 2026

Environment from Lean.Environment.ofKernelEnv has incorrect find?

bugSomething isn't workingSomething isn't working

Status: Open.

#13783 In leanprover/lean4;

· hanwenzhu opened on May 19, 2026

Grind failure: (kernel) application type mismatch

bugSomething isn't workingSomething isn't working

Status: Open.

#13773 In leanprover/lean4;

· HEIGE-PCloud opened on May 18, 2026

Lake compile scheduler can overcommit Lean worker pools on large import graphs, causing macOS SoC watchdog resets

bugSomething isn't workingSomething isn't working

Status: Open.

#13767 In leanprover/lean4;

· elationate opened on May 18, 2026

invalid anchors when passing a typeclass to grind

bugSomething isn't workingSomething isn't working

Status: Open.

#13764 In leanprover/lean4;

· chenson2018 opened on May 17, 2026

Circular wording in #eval docstring

Status: Open.

#13753 In leanprover/lean4;

· thomasjbetsworth opened on May 16, 2026

mepo: score function over-rewards tiny generic theorems

Status: Open.

#13749 In leanprover/lean4;

· kim-em opened on May 16, 2026

#grind_lint does not recognize grind sets

bugSomething isn't workingSomething isn't working

Status: Open.

#13733 In leanprover/lean4;

· chenson2018 opened on May 14, 2026

grind fails when tagging an unrelated lemma

bugSomething isn't workingSomething isn't working

Status: Open.

#13725 In leanprover/lean4;

· fpvandoorn opened on May 13, 2026

Misleading simp mention in cbv error message

bugSomething isn't workingSomething isn't working

Status: Open.

#13719 In leanprover/lean4;

· juanjomadrigal opened on May 12, 2026

RFC: Add Array.mapA

RFCRequest for commentsRequest for comments

Status: Open.

#13714 In leanprover/lean4;

· srghma opened on May 12, 2026