Search results

Declaration ... must be marked as meta error when adding an existing simproc to a custom simp attribute

bugSomething isn't workingSomething isn't working

Status: Open.

#13962 In leanprover/lean4;

· MackieLoeffel opened on Jun 5, 2026

simp unfolds abbrevs when creating auxiliary simp lemmas

bugSomething isn't workingSomething isn't working

Status: Open.

#13958 In leanprover/lean4;

· sgouezel opened on Jun 5, 2026

Grind unknown constant with match and example

bugSomething isn't workingSomething isn't working

Status: Open.

#13950 In leanprover/lean4;

· ericluap opened on Jun 4, 2026

Incorrect parsing of non-indented where declaration followed by declModifiers

bugSomething isn't workingSomething isn't working

Status: Open.

#13934 In leanprover/lean4;

· taterowney opened on Jun 2, 2026

Can't open type as namespace in module

bugSomething isn't workingSomething isn't working

Status: Open.

#13929 In leanprover/lean4;

· frangio opened on Jun 2, 2026

RFC: Std.Path

RFCRequest for commentsRequest for comments

Status: Open.

#13922 In leanprover/lean4;

· algebraic-dev opened on Jun 2, 2026

IR eta reduction/common subexpression elimination on Prods

bugSomething isn't workingSomething isn't working

code-generatorThis issue is with the code generatorThis issue is with the code generator

Status: Open.

#13915 In leanprover/lean4;

· sgraf812 opened on Jun 1, 2026

Lake: path dependencies should share build artifacts with parent workspace

LakeLake related issueLake related issue

Status: Open.

#13913 In leanprover/lean4;

· astefano opened on Jun 1, 2026

mkValueTypeClosure doesn't consider universe constraints

bugSomething isn't workingSomething isn't working

Status: Open.

#13899 In leanprover/lean4;

· Rob23oba opened on May 30, 2026

inaccessible names affect grind?

bugSomething isn't workingSomething isn't working

Status: Open.

#13877 In leanprover/lean4;

· chenson2018 opened on May 29, 2026

withSynthesize tries to solve unrelated universe constraints

bugSomething isn't workingSomething isn't working

Status: Open.

#13875 In leanprover/lean4;

· Rob23oba opened on May 28, 2026

lake lint: support excluding modules from linting

Status: Open.

#13861 In leanprover/lean4;

· astefano opened on May 27, 2026