Skip to content

fix typos that surfaced while creating German translation - #170

Merged
joneugster merged 2 commits into
leanprover-community:mainfrom
TentativeConvert:main
Sep 10, 2026
Merged

joneugster merged 2 commits into
leanprover-community:mainfrom
TentativeConvert:main

Conversation

@TentativeConvert

Copy link
Copy Markdown
Contributor

This PR fixes a few issues we came across while preparing the German translation (PR #162):

  • Multiplication is distributive over addition, not vice versa.
  • command line mode is now called typewriter mode (2 instances)
  • worlds, not levels, have bosses (1 instance)
  • punctuation should be placed outside of $latex$. (1 instance)

@joneugster
joneugster merged commit 913cd4b into leanprover-community:main Sep 10, 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