Skip to content

Pull requests: leanprover/reference-manual

New pull request New
15 Open 613 Closed
15 Open 613 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

doc: expand the lake test and lint driver section HTML available HTML has been generated for this PR
#855 opened May 27, 2026 by kim-em Collaborator Loading…
1
doc: move replace tactic next to have HTML available HTML has been generated for this PR
#852 opened May 23, 2026 by frangio Loading…
1
doc: define trust in "Validating a Lean Proof" HTML available HTML has been generated for this PR
#847 opened May 10, 2026 by OrfeasLitos Contributor Loading…
12
I integrated Violetta's highlights manually.
#846 opened May 7, 2026 by bigmac0 • Draft
1
feat: add more tactic examples and documentation HTML available HTML has been generated for this PR
#843 opened May 6, 2026 by jcreedcmu Contributor Loading…
1
Update Defs.lean: correct description of opaque
#838 opened Apr 23, 2026 by safinaskar Loading…
doc: add lake profile command documentation
#817 opened Mar 30, 2026 by kim-em Collaborator Loading…
perf: Performance scaling for VersoManual HTML available HTML has been generated for this PR
#794 opened Mar 6, 2026 by ejgallego • Draft
1
fix: typo in VCGen/Tutorial.lean
#746 opened Jan 12, 2026 by i-love-lean Loading…
style: upgrade plain backticks to Verso semantic markup
#736 opened Jan 2, 2026 by alok Contributor • Draft
1 task done
1
doc: fix typos and grammar across the manual
#735 opened Jan 2, 2026 by alok Contributor • Draft
feat: add a 'highInferredUniverse' error explanation HTML available HTML has been generated for this PR
#722 opened Dec 27, 2025 by robsimmons Contributor Loading…
8
feat: document well-founded reduction behaviour
#684 opened Dec 5, 2025 by nomeata Collaborator Loading…
1
11
chore: add manual backport instructions to readme HTML available HTML has been generated for this PR
#594 opened Sep 16, 2025 by ashandoak Member Loading…
12
draft: manual entry about iterators and ranges HTML available HTML has been generated for this PR
#580 opened Sep 4, 2025 by datokrat Contributor • Draft
1
ProTip! Filter pull requests by the default branch with base:main.