Issues

• Support BNFs with multiple productions in syntax blocks

  leanprover/reference-manual#966 · Filter by author Vtec234 opened on Oct 6, 2026

• Document lake's new copy feature

  doc-request
  leanprover/reference-manual#955 · Filter by author Garmelon opened on Sep 25, 2026

• Document strong_coinduct

  doc-request
  leanprover/reference-manual#937 · Filter by author wkrozowski opened on Sep 4, 2026

• Document monotonicity_by

  doc-request
  leanprover/reference-manual#936 · Filter by author wkrozowski opened on Sep 4, 2026

• Instances are always exposed

  doc-request
  leanprover/reference-manual#935 · Filter by author faenuccio opened on Sep 3, 2026

• Inductives don't always split parameters from indices with the colon

  leanprover/reference-manual#902 · Filter by author ia0 opened on Jul 16, 2026

• Declaration modifiers don't mention the public visibility

  bug
  leanprover/reference-manual#896 · Filter by author ia0 opened on Jul 15, 2026

• Axioms and Classes disagree on parametricity

  bug
  leanprover/reference-manual#890 · Filter by author ia0 opened on Jul 14, 2026

• Document interaction of namespace and open

  doc-request
  leanprover/reference-manual#884 · Filter by author TwoFX opened on Jul 8, 2026

• Suggested build step fails

  bug
  leanprover/reference-manual#880 · Filter by author Vtec234 opened on Jun 30, 2026
  1

• Invalid link to tests in 12.4.3

  leanprover/reference-manual#878 · Filter by author KislyjKisel opened on Jun 28, 2026

• Document #guard

  doc-request
  leanprover/reference-manual#853 · Filter by author frangio opened on May 24, 2026

• Minor typo in delaborator section

  leanprover/reference-manual#828 · Filter by author alexkeizer opened on Apr 10, 2026

• Link from "extended field notation" to "generalized field notation"

  doc-request
  leanprover/reference-manual#815 · Filter by author TwoFX opened on Mar 25, 2026

• Document where finally

  doc-request
  leanprover/reference-manual#804 · Filter by author j-loreaux opened on Mar 13, 2026

• Document the effect of @[expose]/@[no_expose] on each declaration

  doc-request
  leanprover/reference-manual#771 · Filter by author YaelDillies opened on Feb 2, 2026

• Minor typo in CH14. mapConst documentation

  leanprover/reference-manual#763 · Filter by author hojune-lee opened on Jan 26, 2026

• Traceability of artifacts

  leanprover/reference-manual#748 · Filter by author david-christiansen opened on Jan 15, 2026

• Document valid leanOptions

  doc-request
  leanprover/reference-manual#743 · Filter by author YaelDillies opened on Jan 8, 2026

• 10.4.2: Clarify pipeline syntax

  doc-request
  leanprover/reference-manual#719 · Filter by author AxelBoldt opened on Dec 25, 2025

• Allow set_option documentation

  doc-request
  leanprover/reference-manual#712 · Filter by author robsimmons opened on Dec 17, 2025

• Document new wfrec reduction behavior for Nat-valued measures

  doc-request
  leanprover/reference-manual#680 · Filter by author nomeata opened on Dec 2, 2025
  

• Improve description of grind_pattern

  doc-request
  leanprover/reference-manual#640 · Filter by author david-christiansen opened on Oct 28, 2025

• @ that makes implicit arguments explicit

  doc-request
  leanprover/reference-manual#637 · Filter by author fpvandoorn opened on Oct 27, 2025

• Consider adding "Error explanation:" to error explanatin section headings.

  leanprover/reference-manual#635 · Filter by author jcreedcmu opened on Oct 25, 2025