All pull requests

Pull requests

• refactor: split lake docs into focused modules

  HTML available
  #950·tydeu opened Sep 24, 2026Member·

  ·
  1

• feat: document parser invariants

  #949·david-christiansen opened Sep 23, 2026Collaborator·

  ·

• doc: clarify wording in Annotation.lean

  #930·Hillosanation opened Aug 26, 2026·

  ·

• doc: port mvcgen documentation to vcgen and Std.WP

  HTML available
  #927·sgraf812 opened Aug 21, 2026Contributor·

  ·
  1

• doc: fix typo in infix operators example

  HTML available
  #919·ia0 opened Aug 11, 2026Contributor·

  ·
  1

• chore: fix version in lakefile and add CI check

  #913·david-christiansen opened Aug 6, 2026Collaborator·

  ·

• doc: fix incorrect subsingleton criteria

  HTML available
  #898·ia0 opened Jul 16, 2026Contributor·

  ·
  2

• doc: fix typos in Defs and RecursiveDefs

  HTML available
  #891·ia0 opened Jul 15, 2026Contributor·

  ·
  2

• doc: move replace tactic next to have

  HTML available
  #852·frangio opened May 23, 2026·

  ·
  1

• doc: define trust in "Validating a Lean Proof"

  HTML available
  #847·OrfeasLitos opened May 10, 2026Contributor·

  ·
  12

• feat: add more tactic examples and documentation

  HTML available
  #843·jcreedcmu opened May 6, 2026Collaborator·

  ·
  87

• Update Defs.lean: correct description of opaque

  #838·safinaskar opened Apr 23, 2026·

  ·

• fix: typo in VCGen/Tutorial.lean

  #746·i-love-lean opened Jan 12, 2026·

  ·

• style: upgrade plain backticks to Verso semantic markup

  #736·alok opened Jan 2, 2026Contributor·

  ·
  1

• doc: fix typos and grammar across the manual

  #735·alok opened Jan 2, 2026Contributor·

  ·

• feat: add a 'highInferredUniverse' error explanation

  HTML available
  #722·robsimmons opened Dec 27, 2025Collaborator·

  ·
  8

• feat: document well-founded reduction behaviour

  #684·nomeata opened Dec 5, 2025Collaborator·

  ·
  1

  11

• chore: add manual backport instructions to readme

  HTML available
  #594·ashandoak opened Sep 16, 2025Member·

  ·
  12

• draft: manual entry about iterators and ranges

  HTML available
  #580·datokrat opened Sep 4, 2025Contributor·

  ·
  1