Search results

cases tactic needs to check full body before updating infoview

bugSomething isn't workingSomething isn't working

Status: Open.

#12853 In leanprover/lean4;

· MoritzBeroRoos opened on Mar 9, 2026

Confusing error for <code>let _ ← _</code> before a missing return in the new do elaborator

bugSomething isn't workingSomething isn't working

Status: Open.

#12846 In leanprover/lean4;

· Rob23oba opened on Mar 9, 2026

<code>grind</code> unbounded memory usage (OOM) on <code>Fin 2</code> polynomial equality

bugSomething isn't workingSomething isn't working

Status: Open.

#12842 In leanprover/lean4;

· euprunin opened on Mar 8, 2026

Namespaces from imported modules not visible in module files (namespacesExt asyncMode .local)

Status: Open.

#12833 In leanprover/lean4;

· seanmcl opened on Mar 6, 2026

lake shake removes imports needed by open statements

Status: Open.

#12832 In leanprover/lean4;

· seanmcl opened on Mar 6, 2026

internal exception #3

bugSomething isn't workingSomething isn't working

Status: Open.

#12831 In leanprover/lean4;

· vporton opened on Mar 6, 2026

<code>for ... in ...</code> do elaborator doesn't produce term info

bugSomething isn't workingSomething isn't working

Status: Open.

#12827 In leanprover/lean4;

· Rob23oba opened on Mar 6, 2026

<code>withDuplicableCont</code> leaves continuation metavariable unassigned if <code>checkAssign</code> fails

bugSomething isn't workingSomething isn't working

Status: Open.

#12826 In leanprover/lean4;

· Rob23oba opened on Mar 6, 2026

Import failed, environment already contains <code>sparseCasesOn_2</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#12825 In leanprover/lean4;

· TwoFX opened on Mar 6, 2026

<code>Environment.replay</code> does not support nested inductive types

bugSomething isn't workingSomething isn't working

Status: Open.

#12819 In leanprover/lean4;

· JLimperg opened on Mar 5, 2026

<code>induction</code> tactic swallows IDE diagnostics

bugSomething isn't workingSomething isn't working

Status: Open.

#12815 In leanprover/lean4;

· TwoFX opened on Mar 5, 2026

Verso docstring on <code>where</code> declaration with match causes error

bugSomething isn't workingSomething isn't working

Status: Open.

#12813 In leanprover/lean4;

· Vierkantor opened on Mar 5, 2026