Search results

<code>induction_elim</code> should read <code>cases_elim</code> at one point

bugSomething isn't workingSomething isn't working

Status: Open.

#446 In leanprover/reference-manual;

· david-christiansen opened on May 22, 2025

Incomplete requirements for nested inductive types

bugSomething isn't workingSomething isn't working

Status: Open.

#409 In leanprover/reference-manual;

· arthur-adjedj opened on Mar 31, 2025

Stray <code>variable</code> in example

bugSomething isn't workingSomething isn't working

Status: Open.

#284 In leanprover/reference-manual;

· david-christiansen opened on Feb 4, 2025

ui problem in <code>lifting monad</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#223 In leanprover/reference-manual;

· lengyijun opened on Dec 18, 2024

The description of why strict posivity is needed is wrong

bugSomething isn't workingSomething isn't working

Status: Open.

#124 In leanprover/reference-manual;

· david-christiansen opened on Oct 24, 2024