Search results

<code>rw</code> tactic "steals" goals (again)

bugSomething isn't workingSomething isn't working

Status: Open.

#12135 In leanprover/lean4;

· TwoFX opened on Jan 24, 2026

Verso docstrings with unmatched closing bracket cause misleading error message

bugSomething isn't workingSomething isn't working

Status: Open.

#12118 In leanprover/lean4;

· datokrat opened on Jan 23, 2026

XML parser for !DOCTYPE does not handle spaces in PubidLiteral

bugSomething isn't workingSomething isn't working

Status: Open.

#12109 In leanprover/lean4;

· halfaya opened on Jan 22, 2026

Universe normalization is too late to prevent unfolding in defeq check

Status: Open.

#12102 In leanprover/lean4;

· kbuzzard opened on Jan 22, 2026

#eval (- 2 ^ 63 : ISize) / (-1) crashes

bugSomething isn't workingSomething isn't working

Status: Open.

#12097 In leanprover/lean4;

· eric-wieser opened on Jan 21, 2026

Possible deadlock on task manager finalization / shutdown when threads are being throttled by max_std_workers

bugSomething isn't workingSomething isn't working

Status: Open.

#12094 In leanprover/lean4;

· marcelolynch opened on Jan 21, 2026

<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 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