All pull requests

Pull requests

• feat: check that verso dependency targets the right bump branch

  HTML available
  #987·robsimmons opened Oct 30, 2026Collaborator·

  ·
  1

• feat: Lean as a Library chapter

  HTML available
  #984·Vtec234 opened Oct 29, 2026Member·2/3·

  ·
  1

• feat: document external kernels and export format

  HTML available
  #982·david-christiansen opened Oct 29, 2026Collaborator·

  ·
  1

• feat: section on widgets

  HTML available
  #977·Vtec234 opened Oct 25, 2026Member·3/3·

  ·

• feat: document HTML and JSON libraries

  HTML available
  #965·Vtec234 opened Oct 4, 2026Member·1/3·

  ·
  71

• doc: fix link to the extern interpreter example

  HTML available
  #960·fushanbobfan opened Sep 28, 2026·

  ·
  1

  1

• doc: cover more of lake cache

  HTML available
  #956·tydeu opened Sep 26, 2026Member·

  ·
  37

• feat: document parser invariants

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

  ·

• doc: clarify wording in Annotation.lean

  #930·Hillosanation opened Aug 26, 2026·

  ·

• 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 task done·

  ·
  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