Skip to content

Add pt-BR translation #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
felipponn wants to merge 16 commits into from
Closed

Add pt-BR translation #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
90902a7
chore: Update link to lean 3 version of the natural number game to po…
Osalotioman Dec 27, 2025
1853318
2 typos (#123)
TentativeConvert Dec 27, 2025
7dc9e92
"Leave World" button is now called "Home" (#120)
TentativeConvert Dec 27, 2025
7af99fd
stray quotation mark at the end of definition of Add (#121)
TentativeConvert Dec 27, 2025
d593c1e
Fix minor spelling error in L3 of Implication World (#124)
vatrat Dec 27, 2025
6367e71
chore: update button text from 'Leave World' to 'Home' (#127)
he7d3r Mar 1, 2026
b2b47e2
undo change in spelling (#133)
joneugster Mar 16, 2026
dfad655
Fix Minor Typos encontered when plyaing the game. (#128)
ThomasMoulin-hub Mar 16, 2026
4cd29af
add missing period in README.md (#130)
yerke Mar 16, 2026
b85b080
use targeted (#134)
joneugster Mar 16, 2026
dfa53e9
Minor documentation improvements (#136)
marlycormar May 23, 2026
fdef6fe
Leave World -> Home (#150)
comods May 23, 2026
727e4d2
Fix few typos (#156)
jhrcek Jul 3, 2026
360d797
Fix typos in L06intro.lean (#168)
armgabrielyan Aug 30, 2026
b0d93b1
Start translation to pt-BR
felipponn Sep 6, 2026
f998483
Finish pt-BR translation
felipponn Sep 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions .i18n/en/Game.pot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ msgid "Nice!\n"
"The next step in the development of order theory is to develop\n"
"the theory of the interplay between §0 and multiplication.\n"
"If you've already done Multiplication World, you're now ready for\n"
"Advanced Multiplication World. Click on \"Leave World\" to access it."
"Advanced Multiplication World. Click on \"Home\" to access it."
msgstr ""

#. §0: `a + b + c`
Expand Down Expand Up @@ -206,7 +206,7 @@ msgid "Here's my proof:\n"
"World, a more computer-sciency world, we will develop machinery which makes\n"
"questions like this much easier, and goals like §1 feasible.\n"
"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
"the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\n"
"the lemmas needed to get a working theory of inequalities. Click \"Home\" and\n"
"decide your route."
msgstr ""

Expand Down Expand Up @@ -387,7 +387,7 @@ msgstr ""
#. §1: `b`
#. §2: `d`
#: Game.Levels.Algorithm.L02add_algo1
msgid "Finally use a targetted §0 to switch §1 and §2"
msgid "Finally use a targeted §0 to switch §1 and §2"
msgstr ""

#. §0: `repeat t`
Expand Down Expand Up @@ -1017,7 +1017,7 @@ msgid "§0, with notation §1, is\n"
"* §3\n"
"\n"
"Other theorems about naturals, such as §4, are proved\n"
"by induction using these two basic theorems.\""
"by induction using these two basic theorems."
msgstr ""

#. §0: $x+1=4$
Expand Down Expand Up @@ -1744,7 +1744,7 @@ msgid "*Game version: 4.3*\n"
"## Resources\n"
"\n"
"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
"* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n"
"* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n"
"\n"
"## Problems?\n"
"\n"
Expand Down Expand Up @@ -1800,7 +1800,7 @@ msgid "Here is an example proof of 2+2=4 showing off various techniques.\n"
"move back into \"Typewriter mode\".\n"
"\n"
"You have finished tutorial world!\n"
"Click \"Leave World\" to go back to the\n"
"Click \"Home\" to go back to the\n"
"overworld, and select Addition World, where you will learn\n"
"about the §3 tactic."
msgstr ""
Expand Down Expand Up @@ -1970,7 +1970,7 @@ msgid "§0 is a proof that §1. But if your goal\n"
"You don't need induction. §7 moves brackets around,\n"
"and §8 moves variables around.\n"
"\n"
"Remember that you can do more targetted rewrites by\n"
"Remember that you can do more targeted rewrites by\n"
"adding explicit variables as inputs to theorems. For example §9\n"
"will only do rewrites of the form §10, and §11\n"
"will only do rewrites of the form §12."
Expand Down Expand Up @@ -2147,7 +2147,7 @@ msgid "## Summary\n"
"If you can't remember the name of the proof of an equality, look it up in\n"
"the list of lemmas on the right.\n"
"\n"
"## Targetted usage\n"
"## Targeted usage\n"
"\n"
"If your goal is §67 and you want to rewrite §68\n"
"to §69, then §70 will not work because Lean finds another\n"
Expand Down Expand Up @@ -2636,7 +2636,7 @@ msgid "How about this for a proof:\n"
"§0\n"
"\n"
"That's the end of Advanced Addition World! You'll need these theorems\n"
"for the next world, §1 World. Click on \"Leave World\" to access it."
"for the next world, §1 World. Click on \"Home\" to access it."
msgstr ""

#. §0: `n`
Expand Down Expand Up @@ -4241,7 +4241,7 @@ msgid "You've now seen all the tactics you need to beat the final boss of the ga
"World. These tactics let you prove more facts about addition, such as\n"
"how to deduce §0 from §1.\n"
"\n"
"Click \"Leave World\" and make your choice."
"Click \"Home\" and make your choice."
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
Expand Down
50 changes: 25 additions & 25 deletions .i18n/fr/Game.json
View file
Open in desktop

Large diffs are not rendered by default.

54 changes: 27 additions & 27 deletions .i18n/fr/Game.po
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ msgid ""
"If you can't remember the name of the proof of an equality, look it up in\n"
"the list of lemmas on the right.\n"
"\n"
"## Targetted usage\n"
"## Targeted usage\n"
"\n"
"If your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\n"
"to `c + a`, then `rw [add_comm]` will not work because Lean finds another\n"
Expand Down Expand Up @@ -513,7 +513,7 @@ msgstr ""
"apparaître dans le jeu des nombres naturels.*"

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`one_eq_succ_zero` is a proof of `1 = succ 0`.\""
msgid "`one_eq_succ_zero` is a proof of `1 = succ 0`."
msgstr "`one_eq_succ_zero` est une preuve que `1 = succ 0`."

#: Game.Levels.Tutorial.L03two_eq_ss0
Expand Down Expand Up @@ -663,7 +663,7 @@ msgid ""
"* `add_succ a b : a + succ b = succ (a + b)`\n"
"\n"
"Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\n"
"by induction using these two basic theorems.\""
"by induction using these two basic theorems."
msgstr ""
"`Add a b`, avec la notation `a + b`, est\n"
"la somme habituelle des nombres naturels. En interne, elle est définie\n"
Expand All @@ -674,7 +674,7 @@ msgstr ""
"* `add_succ a b : a + succ b = succ (a + b)`\n"
"\n"
"D'autres théorèmes sur les naturels, comme `zero_add a : 0 + a = a`, sont prouvés\n"
"par induction en utilisant ces deux théorèmes de base.\""
"par induction en utilisant ces deux théorèmes de base."

#: Game.Levels.Tutorial.L05add_zero
msgid ""
Expand Down Expand Up @@ -980,7 +980,7 @@ msgid ""
"move back into \"Typewriter mode\".\n"
"\n"
"You have finished tutorial world!\n"
"Click \"Leave World\" to go back to the\n"
"Click \"Home\" to go back to the\n"
"overworld, and select Addition World, where you will learn\n"
"about the `induction` tactic."
msgstr ""
Expand Down Expand Up @@ -1083,14 +1083,14 @@ msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid ""
"`zero_add x` is the proof of `0 + x = x`.\n"
"`zero_add n` is the proof of `0 + n = n`.\n"
"\n"
"`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\n"
"`zero_add` is a `simp` lemma, because replacing `0 + n` by `n`\n"
"is almost always what you want to do if you're simplifying an expression."
msgstr ""
"`zero_add x` est la preuve que `0 + x = x`.\n"
"`zero_add n` est la preuve que `0 + n = n`.\n"
"\n"
"`zero_add` est un lemme `simp`, car remplacer `0 + x` par `x`\n"
"`zero_add` est un lemme `simp`, car remplacer `0 + n` par `n`\n"
"est presque toujours ce que vous voulez faire si vous simplifiez une expression."

#: Game.Levels.Addition.L01zero_add
Expand Down Expand Up @@ -1285,8 +1285,8 @@ msgstr ""
"Cela devrait suffire."

#: Game.Levels.Addition.L03add_comm
msgid "`add_comm x y` is a proof of `x + y = y + x`."
msgstr "`add_comm x y` est une preuve de `x + y = y + x`."
msgid "`add_comm a b` is a proof of `a + b = b + a`."
msgstr "`add_comm a b` est une preuve de `a + b = b + a`."

#: Game.Levels.Addition.L03add_comm
msgid ""
Expand Down Expand Up @@ -1391,7 +1391,7 @@ msgid ""
"You don't need induction. `add_assoc` moves brackets around,\n"
"and `add_comm` moves variables around.\n"
"\n"
"Remember that you can do more targetted rewrites by\n"
"Remember that you can do more targeted rewrites by\n"
"adding explicit variables as inputs to theorems. For example `rw [add_comm b]`\n"
"will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\n"
"will only do rewrites of the form `b + c = c + b`."
Expand Down Expand Up @@ -1439,7 +1439,7 @@ msgid ""
"World. These tactics let you prove more facts about addition, such as\n"
"how to deduce `a = 0` from `x + a = x`.\n"
"\n"
"Click \"Leave World\" and make your choice."
"Click \"Home\" and make your choice."
msgstr ""
"Vous avez maintenant vu toutes les tactiques nécessaires pour vaincre le boss final du jeu.\n"
"Vous pouvez commencer le voyage vers ce boss en entrant dans le monde de la Multiplication.\n"
Expand Down Expand Up @@ -1560,11 +1560,11 @@ msgstr ""

#: Game.Levels.Multiplication.L02zero_mul
msgid ""
"`zero_mul x` is the proof that `0 * x = 0`.\n"
"`zero_mul m` is the proof that `0 * m = 0`.\n"
"\n"
"Note: `zero_mul` is a `simp` lemma."
msgstr ""
"`zero_mul x` est la preuve que `0 * x = 0`.\n"
"`zero_mul m` est la preuve que `0 * m = 0`.\n"
"\n"
"Note : `zero_mul` est un lemme `simp`."

Expand Down Expand Up @@ -1973,7 +1973,7 @@ msgid ""
"Note in particular that `0 ^ 0 = 1`."
msgstr ""
"`Pow a b`, avec la notation `a ^ b`, est l'exponentiation\n"
" habituelle des nombres naturels, c'est à dire `a` puissance `b. En interne, elle est\n"
" habituelle des nombres naturels, c'est à dire `a` puissance `b`. En interne, elle est\n"
" définie par deux axiomes :\n"
"\n"
" * `pow_zero a : a ^ 0 = 1`\n"
Expand Down Expand Up @@ -2248,7 +2248,7 @@ msgid ""
"an interactive textbook which you can read in your browser,\n"
"and which explains how to work with many more mathematical concepts in Lean."
msgstr ""
"Nous avons maintenant suffisamment de connaissance pour énoncer une version mathématiquement "
"Nous avons maintenant suffisamment de connaissances pour énoncer une version mathématiquement "
"exacte, mais un peu\n"
"maladroite, du \"grand théorème de Fermat\".\n"
"\n"
Expand Down Expand Up @@ -2787,7 +2787,7 @@ msgid ""
"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\n"
"in Lean. We do this with the `intro` tactic."
msgstr ""
"Nous avons vu comment utilsier `apply` sur des théorèmes et des hypothèses\n"
"Nous avons vu comment utiliser `apply` sur des théorèmes et des hypothèses\n"
"de la forme `P → Q`. Mais que faire si notre *but* est de la forme `P → Q` ?\n"
"Pour prouver ce but, nous devons savoir dire \"supposons `P` et déduisons `Q`\"\n"
"dans Lean. Nous faisons cela avec la tactique `intro`."
Expand Down Expand Up @@ -3108,7 +3108,7 @@ msgid ""
"World, a more computer-sciency world, we will develop machinery which makes\n"
"questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\n"
"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
"the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\n"
"the lemmas needed to get a working theory of inequalities. Click \"Home\" and\n"
"decide your route."
msgstr ""
"Voici ma preuve :\n"
Expand Down Expand Up @@ -3244,7 +3244,7 @@ msgstr ""
"gauche."

#: Game.Levels.Algorithm.L02add_algo1
msgid "Finally use a targetted `add_comm` to switch `b` and `d`"
msgid "Finally use a targeted `add_comm` to switch `b` and `d`"
msgstr "Enfin, utilisez un `add_comm` ciblé pour échanger `b` et `d`"

#: Game.Levels.Algorithm.L02add_algo1
Expand Down Expand Up @@ -4114,7 +4114,7 @@ msgid ""
"```\n"
"\n"
"That's the end of Advanced Addition World! You'll need these theorems\n"
"for the next world, `≤` World. Click on \"Leave World\" to access it."
"for the next world, `≤` World. Click on \"Home\" to access it."
msgstr ""
"Que pensez-vous de cette preuve :\n"
"\n"
Expand Down Expand Up @@ -4171,7 +4171,7 @@ msgid ""
msgstr ""
"## Résumé\n"
"\n"
"La tactique `use` fait progresser les buts qui affirement que quelque chose *existe*.\n"
"La tactique `use` fait progresser les buts qui affirment que quelque chose *existe*.\n"
"Si le but affirme qu'un certain `x` existe avec une certaine propriété, et que vous savez\n"
"que `x = 37` fonctionnera, alors `use 37` fera progresser.\n"
"\n"
Expand Down Expand Up @@ -4279,7 +4279,7 @@ msgid ""
"If you `use` the wrong number, you get stuck with a goal you can't prove.\n"
"What number will you `use` here?"
msgstr ""
"Si vous utiliser `use` avec le mauvais nombre, vous restez bloqué avec un but que vous ne pourrez "
"Si vous utilisez `use` avec le mauvais nombre, vous restez bloqué avec un but que vous ne pourrez "
"pas prouver.\n"
"Quel nombre allez-vous choisir ici ?"

Expand Down Expand Up @@ -4769,7 +4769,7 @@ msgid ""
"The next step in the development of order theory is to develop\n"
"the theory of the interplay between `≤` and multiplication.\n"
"If you've already done Multiplication World, you're now ready for\n"
"Advanced Multiplication World. Click on \"Leave World\" to access it."
"Advanced Multiplication World. Click on \"Home\" to access it."
msgstr ""
"Bien !\n"
"\n"
Expand Down Expand Up @@ -4982,7 +4982,7 @@ msgid ""
"To help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\n"
"on the right to see what it does."
msgstr ""
"La multiplication transforme généralement un nombre en un noùmbre plus grand, mais la "
"La multiplication transforme généralement un nombre en un nombre plus grand, mais la "
"multiplication par zéro peut le rendre\n"
"plus petit. Ainsi, de nombreux lemmes sur les inégalités et la multiplication nécessitent l'\n"
"hypothèse `a ≠ 0`. Voici un lemme clé qui nous permet d'utiliser cette hypothèse.\n"
Expand Down Expand Up @@ -5503,7 +5503,7 @@ msgid ""
"## Resources\n"
"\n"
"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
"* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no "
"* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no "
"longer maintained)\n"
"\n"
"## Problems?\n"
Expand Down Expand Up @@ -5550,7 +5550,7 @@ msgstr ""
"## Ressources\n"
"\n"
"* Le forum [Lean Zulip chat](https://leanprover.zulipchat.com/)\n"
"* [Version Lean3 originale](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (non "
"* [Version Lean3 originale](https://github.com/ImperialCollegeLondon/natural_number_game/) (non "
"maintenue)\n"
"\n"
"## Problèmes ?\n"
Expand Down
Loading