Skip to content

Minor documentation improvements#136

Merged
joneugster merged 5 commits into
leanprover-community:mainfrom
marlycormar:pr-improve-docs
May 23, 2026
Merged

Minor documentation improvements#136
joneugster merged 5 commits into
leanprover-community:mainfrom
marlycormar:pr-improve-docs

Conversation

@marlycormar

@marlycormar marlycormar commented Apr 8, 2026

Copy link
Copy Markdown
Contributor

Thanks for developing the NNG4 game!

I found a few minor documentation issues, which this PR addresses. I am not entirely sure which notation standard you would prefer throughout the game, so I made an informed choice by aligning the notation with the initial statement in each case. I also updated the corresponding files used for translating the documentation into other languages so that these changes remain consistent across the project.

As I continue working through the game, I would be happy to open additional PRs if I come across other minor issues.

Summary of changes

  • Removed dangling end quotes from one_eq_succ_zero and updated the corresponding translation files.
  • Removed dangling end quotes from + and updated the corresponding translation files.
  • add_comm used both $a/b$ and $x/y$; I aligned the notation to use $a$ and $b$ throughout and updated the corresponding translation files.
  • zero_add used both $n$ and $x$; I aligned the notation to use $n$ throughout and updated the corresponding translation files.
  • zero_mul used both $m$ and $x$; I aligned the notation to use $m$ throughout and updated the corresponding translation files.

@joneugster joneugster left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you!

I personally think the variable renaming is kind of superfluous and as inconsistent as it was before, but now it's here, let's just merge this as-is

@joneugster joneugster merged commit dfa53e9 into leanprover-community:main May 23, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants