Skip to content

Pull requests: leanprover-community/NNG4

New pull request New
Clear current search query, filters, and sorts
4 Open 63 Closed
4 Open 63 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

use targeted
#134 by joneugster Collaborator was merged Mar 16, 2026 Loading…
1
undo change in spelling
#133 by joneugster Collaborator was merged Mar 16, 2026 Loading…
Fix typo in rw tactic description
#132 by AaronSzaboo was closed Mar 16, 2026 Loading…
5
add missing period in README.md
#130 by yerke Contributor was merged Mar 16, 2026 Loading…
Fix Minor Typos encontered when plyaing the game.
#128 by ThomasMoulin-hub Contributor was merged Mar 16, 2026 Loading…
2
chore: update button text from 'Leave World' to 'Home'
#127 by he7d3r Contributor was merged Mar 1, 2026 Loading…
1
chore: Update link to lean 3 version of the natural number game to point to the frozen game repo
#126 by Osalotioman Contributor was merged Dec 27, 2025 Loading…
1
1
Fix minor spelling error in L3 of Implication World
#124 by vatrat Contributor was merged Dec 27, 2025 Loading…
1
2 typos
#123 by TentativeConvert Contributor was merged Dec 27, 2025 Loading…
1
stray quotation mark at the end of definition of Add
#121 by TentativeConvert Contributor was merged Dec 27, 2025 Loading…
1
"Leave World" button is now called "Home"
#120 by TentativeConvert Contributor was merged Dec 27, 2025 Loading…
1
fix: remove dot notation on MyNat.succ
#119 by kbuzzard Member was merged Sep 28, 2025 Loading…
Clarify introduction: Lean is a language
#118 by dharmatech Contributor was closed Sep 28, 2025 Loading…
@kbuzzard
3
Typo: remove extra word to
#117 by dharmatech Contributor was merged Sep 27, 2025 Loading…
Fix typo in Game
#116 by bearomorphism Contributor was merged Sep 27, 2025 Loading…
Fix typo in readme
#115 by bearomorphism Contributor was merged Sep 27, 2025 Loading…
chore: bump v4.23.0
#113 by joneugster Collaborator was merged Sep 27, 2025 Loading…
1
fix: adjust hint text
#112 by joneugster Collaborator was merged Sep 23, 2025 Loading…
French translation (for a new Pull Request)
#108 by arnbod Contributor was merged Jul 11, 2025 Loading…
2
Remove extra space, that prevent translation
#107 by arnbod Contributor was merged Sep 23, 2025 Loading…
French translation
#106 by arnbod Contributor was closed Jul 11, 2025 Loading…
6
Add regenerated JSON file from last review
#105 by kant2002 Contributor was merged Jul 10, 2025 Loading…
Small Typo Fix In L07or_symm.lean
#100 by cjl8zf was merged Sep 23, 2025 Loading…
Ukrainian translation
#95 by kant2002 Contributor was merged Jul 10, 2025 Loading…
20
Translation maintenance enhancement New feature or request
#94 by dalps Contributor was merged Sep 26, 2025 Loading…
5
ProTip! Follow long discussions with comments:>50.