Search results

<code>instance</code> command should reject instances of non-class types

bugSomething isn't workingSomething isn't working

Status: Open.

#12075 In leanprover/lean4;

· NicolasRouquette opened on Jan 20, 2026

RFC: Separate out <code>doc.verso</code> option between module docs and declaration docs

RFCRequest for commentsRequest for comments

Status: Open.

#12070 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso docstring appears to ignore header on 0th line

bugSomething isn't workingSomething isn't working

Status: Open.

#12067 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso docstrings on <code>where</code>-clause declaration cause errors

bugSomething isn't workingSomething isn't working

Status: Open.

#12066 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso docstrings and <code>#guard_msgs</code> cause panic: unexpected context-free info tree node

bugSomething isn't workingSomething isn't working

Status: Open.

#12065 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso suggests adding <code>+error</code> to suppress warnings

bugSomething isn't workingSomething isn't working

Status: Open.

#12064 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso docstring syntax error messages do not suggest correct fixes

bugSomething isn't workingSomething isn't working

Status: Open.

#12063 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Verso module doc syntax error causes "Unsupported syntax: failed to pretty-print term"

bugSomething isn't workingSomething isn't working

Status: Open.

#12062 In leanprover/lean4;

· Vierkantor opened on Jan 20, 2026

Range syntax has bad precedence compared to <code>|&gt;.</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#12055 In leanprover/lean4;

· TwoFX opened on Jan 20, 2026

RFC: generalize basic Inhabited/Nonempty instances from Monad to Applicative

RFCRequest for commentsRequest for comments

Status: Open.

#12042 In leanprover/lean4;

· fgdorais opened on Jan 19, 2026

simp attribute + unknown identifiers = internal exception #3 / PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:448:17: unknown metavariable

bugSomething isn't workingSomething isn't working

Status: Open.

#12020 In leanprover/lean4;

· Julian opened on Jan 15, 2026

lake update nonexistant-pkgs does not complain

bugSomething isn't workingSomething isn't working

Status: Open.

#12005 In leanprover/lean4;

· nomeata opened on Jan 14, 2026