greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

run msguniq on Game.pot

Browse Source
This commit is contained in:
Federico
2025-03-19 21:50:06 +01:00
committed by dalps
parent 869e254313
commit 26eeb2ea7c
1 changed files with 56 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

83
.i18n/en/Game.pot
View File

@@ -721,7 +721,8 @@ msgid "## Summary\n"
msgstr "" msgstr ""
#: Game.Levels.Addition.L05add_right_comm #: Game.Levels.Addition.L05add_right_comm
msgid "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n" msgid ""
"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n"
"\n" "\n"
"In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\n" "In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\n"
"as `a + b + c = a + c + b`." "as `a + b + c = a + c + b`."
@@ -927,7 +928,8 @@ msgid "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b
msgstr "" msgstr ""
#: Game.Levels.Multiplication.L07mul_add #: Game.Levels.Multiplication.L07mul_add
msgid "Multiplication distributes\n" msgid ""
"Multiplication distributes\n"
"over addition on the left.\n" "over addition on the left.\n"
"\n" "\n"
"`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`." "`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`."
@@ -962,7 +964,9 @@ msgid "add_left_eq_self"
msgstr "" msgstr ""
#: Game.Levels.Multiplication #: Game.Levels.Multiplication
msgid "How should we define `37 * x`? Just like addition, we need to give definitions\n" msgid ""
"How should we define `37 * x`? Just like addition, we need to give "
"definitions\n"
"when $x=0$ and when $x$ is a successor.\n" "when $x=0$ and when $x$ is a successor.\n"
"\n" "\n"
"The zero case is easy: we define `37 * 0` to be `0`. Now say we know\n" "The zero case is easy: we define `37 * 0` to be `0`. Now say we know\n"
@@ -974,8 +978,10 @@ msgid "How should we define `37 * x`? Just like addition, we need to give defini
" * `mul_zero a : a * 0 = 0`\n" " * `mul_zero a : a * 0 = 0`\n"
" * `mul_succ a d : a * succ d = a * d + a`\n" " * `mul_succ a d : a * succ d = a * d + a`\n"
"\n" "\n"
"In this world, we must not only prove facts about multiplication like `a * b = b * a`,\n" "In this world, we must not only prove facts about multiplication like `a * b "
"we must also prove facts about how multiplication interacts with addition, like `a * (b + c) = a * b + a * c`.\n" "= b * a`,\n"
"we must also prove facts about how multiplication interacts with addition, "
"like `a * (b + c) = a * b + a * c`.\n"
"Let's get started." "Let's get started."
msgstr "" msgstr ""
@@ -1367,7 +1373,8 @@ msgid "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`."
msgstr "" msgstr ""
#: Game.Levels.Implication.L04succ_inj #: Game.Levels.Implication.L04succ_inj
msgid "# Statement\n" msgid ""
"# Statement\n"
"\n" "\n"
"If $a$ and $b$ are numbers, then\n" "If $a$ and $b$ are numbers, then\n"
"`succ_inj a b` is the proof that\n" "`succ_inj a b` is the proof that\n"
@@ -1384,7 +1391,8 @@ msgid "# Statement\n"
"You can think of `succ_inj` itself as a proof; it is the proof\n" "You can think of `succ_inj` itself as a proof; it is the proof\n"
"that `succ` is an injective function. In other words,\n" "that `succ` is an injective function. In other words,\n"
"`succ_inj` is a proof of\n" "`succ_inj` is a proof of\n"
"$\\forall a, b \\in \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n" "$\\forall a, b \\in \\mathbb{N}, ( \\operatorname{succ}(a) = "
"\\operatorname{succ}(b)) \\implies a=b$.\n"
"\n" "\n"
"`succ_inj` was postulated as an axiom by Peano, but\n" "`succ_inj` was postulated as an axiom by Peano, but\n"
"in Lean it can be proved using `pred`, a mathematically\n" "in Lean it can be proved using `pred`, a mathematically\n"
@@ -1734,7 +1742,8 @@ msgid "If `a` and `b` are numbers, then `succ_inj a b` is a proof\n"
msgstr "" msgstr ""
#: Game.Levels.Algorithm.L02add_algo1 #: Game.Levels.Algorithm.L02add_algo1
msgid "In some later worlds, we're going to see some much nastier levels,\n" msgid ""
"In some later worlds, we're going to see some much nastier levels,\n"
"like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\n" "like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\n"
"Brackets need to be moved around, and variables need to be swapped.\n" "Brackets need to be moved around, and variables need to be swapped.\n"
"\n" "\n"
@@ -2145,7 +2154,8 @@ msgid "We now have enough to prove that multiplication is associative,\n"
msgstr "" msgstr ""
#: Game.Levels.AdvAddition.L04add_right_eq_self #: Game.Levels.AdvAddition.L04add_right_eq_self
msgid "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n" msgid ""
"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n"
"Two ways to do it spring to mind; I'll mention them when you've solved it." "Two ways to do it spring to mind; I'll mention them when you've solved it."
msgstr "" msgstr ""
@@ -2167,23 +2177,33 @@ msgid "Now finish in one line."
msgstr "" msgstr ""
#: Game.Levels.AdvAddition.L05add_right_eq_zero #: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\n" msgid ""
"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` "
"and `b = 0`.\n"
"Let's prove one of these facts in this level, and the other in the next.\n" "Let's prove one of these facts in this level, and the other in the next.\n"
"\n" "\n"
"## A new tactic: `cases`\n" "## A new tactic: `cases`\n"
"\n" "\n"
"The `cases` tactic will split an object or hypothesis up into the possible ways\n" "The `cases` tactic will split an object or hypothesis up into the possible "
"ways\n"
"that it could have been created.\n" "that it could have been created.\n"
"\n" "\n"
"For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\n" "For example, sometimes you want to deal with the two cases `b = 0` and `b = "
"but don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\n" "succ d` separately,\n"
"In this situation you can use `cases b with d` instead. There are two ways to make\n" "but don't need the inductive hypothesis `hd` that comes with `induction b "
"a number: it's either zero or a successor. So you will end up with two goals, one\n" "with d hd`.\n"
"In this situation you can use `cases b with d` instead. There are two ways "
"to make\n"
"a number: it's either zero or a successor. So you will end up with two "
"goals, one\n"
"with `b = 0` and one with `b = succ d`.\n" "with `b = 0` and one with `b = succ d`.\n"
"\n" "\n"
"Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies\n" "Another example: if you have a hypothesis `h : False` then you are done, "
"any statement. Here `cases h` will close the goal, because there are *no* ways to\n" "because a false statement implies\n"
"make a proof of `False`! So you will end up with no goals, meaning you have proved everything." "any statement. Here `cases h` will close the goal, because there are *no* "
"ways to\n"
"make a proof of `False`! So you will end up with no goals, meaning you have "
"proved everything."
msgstr "" msgstr ""
#: Game #: Game
@@ -2240,7 +2260,8 @@ msgid "Let's now begin our approach to the final boss,\n"
msgstr "" msgstr ""
#: Game.Levels.AdvAddition.L06add_left_eq_zero #: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid "How about this for a proof:\n" msgid ""
"How about this for a proof:\n"
"\n" "\n"
"```\n" "```\n"
"rw [add_comm]\n" "rw [add_comm]\n"
@@ -2640,7 +2661,8 @@ msgid "Let's now learn about Peano's second axiom for addition, `add_succ`."
msgstr "" msgstr ""
#: Game.Levels.LessOrEqual.L09succ_le_succ #: Game.Levels.LessOrEqual.L09succ_le_succ
msgid "Here's my proof:\n" msgid ""
"Here's my proof:\n"
"```\n" "```\n"
"cases hx with d hd\n" "cases hx with d hd\n"
"use d\n" "use d\n"
@@ -2980,15 +3002,18 @@ msgid "For all natural numbers $a$ and $b$, we have\n"
msgstr "" msgstr ""
#: Game.Levels.AdvMultiplication.L06mul_right_eq_one #: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "# Summary\n" msgid ""
"# Summary\n"
"\n" "\n"
"The `have` tactic can be used to add new hypotheses to a level, but of course\n" "The `have` tactic can be used to add new hypotheses to a level, but of "
"course\n"
"you have to prove them.\n" "you have to prove them.\n"
"\n" "\n"
"\n" "\n"
"## Example\n" "## Example\n"
"\n" "\n"
"The simplest usage is like this. If you have `a` in your context and you execute\n" "The simplest usage is like this. If you have `a` in your context and you "
"execute\n"
"\n" "\n"
"`have ha : a = 0`\n" "`have ha : a = 0`\n"
"\n" "\n"
@@ -3302,7 +3327,8 @@ msgid "`zero_mul x` is the proof that `0 * x = 0`.\n"
msgstr "" msgstr ""
#: Game #: Game
msgid "# Welcome to the Natural Number Game\n" msgid ""
"# Welcome to the Natural Number Game\n"
"#### An introduction to mathematical proof.\n" "#### An introduction to mathematical proof.\n"
"\n" "\n"
"In this game, we will build the basic theory of the natural\n" "In this game, we will build the basic theory of the natural\n"
@@ -3322,12 +3348,15 @@ msgid "# Welcome to the Natural Number Game\n"
"Note: this is a new Lean 4 version of the game containing several\n" "Note: this is a new Lean 4 version of the game containing several\n"
"worlds which were not present in the old Lean 3 version. More new worlds\n" "worlds which were not present in the old Lean 3 version. More new worlds\n"
"such as Strong Induction World, Even/Odd World and Prime Number World\n" "such as Strong Induction World, Even/Odd World and Prime Number World\n"
"are in development; if you want to see their state or even help out, checkout\n" "are in development; if you want to see their state or even help out, "
"out the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n" "checkout\n"
"out the [issues in the github repo](https://github.com/leanprover-community/"
"NNG4/issues).\n"
"\n" "\n"
"## More\n" "## More\n"
"\n" "\n"
"Click on the three lines in the top right and select \"Game Info\" for resources,\n" "Click on the three lines in the top right and select \"Game Info\" for "
"resources,\n"
"links, and ways to interact with the Lean community." "links, and ways to interact with the Lean community."
msgstr "" msgstr ""