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

chore: update Game.pot .

Browse Source
This commit is contained in:
Kevin Buzzard
2025-03-14 17:07:36 +00:00
parent a022b0673d
commit a238f74e54
1 changed files with 38 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

45
.i18n/en/Game.pot
View File

@@ -1,7 +1,7 @@
msgid "" msgid ""
msgstr "Project-Id-Version: Game v4.7.0\n" msgstr "Project-Id-Version: Game v4.7.0\n"
"Report-Msgid-Bugs-To: \n" "Report-Msgid-Bugs-To: \n"
"POT-Creation-Date: Sat Feb 1 23:22:17 2025\n" "POT-Creation-Date: Fri Mar 14 17:06:47 2025\n"
"Last-Translator: \n" "Last-Translator: \n"
"Language-Team: none\n" "Language-Team: none\n"
"Language: en\n" "Language: en\n"
@@ -1599,8 +1599,11 @@ msgid "## Summary\n"
msgstr "" msgstr ""
#: Game.Levels.Implication.L03apply #: Game.Levels.Implication.L03apply
msgid "In this level one of our hypotheses is an *implication*. We can use this\n" msgid "In this level, the hypotheses `h2` is an *implication*. It says\n"
"hypothesis with the `apply` tactic." "that *if* `x = 37` *then* `y = 42`. We can use this\n"
"hypothesis with the `apply` tactic. Remember you can click on\n"
"`apply` or any other tactic on the right to see a detailed explanation\n"
"of what it does, with examples."
msgstr "" msgstr ""
#: Game.Levels.Implication.L03apply #: Game.Levels.Implication.L03apply
@@ -1797,7 +1800,7 @@ msgstr ""
#: Game.Levels.Implication.L07intro2 #: Game.Levels.Implication.L07intro2
msgid "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\n" msgid "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\n"
"change `succ x = succ y`." "change `h` to `succ x = succ y`."
msgstr "" msgstr ""
#: Game.Levels.Implication.L07intro2 #: Game.Levels.Implication.L07intro2
@@ -2381,7 +2384,8 @@ msgstr ""
#: Game.Levels.Algorithm.L09decide2 #: Game.Levels.Algorithm.L09decide2
msgid "Congratulations! You've finished Algorithm World. These algorithms\n" msgid "Congratulations! You've finished Algorithm World. These algorithms\n"
"will be helpful for you in Even-Odd World." "will be helpful for you in Even-Odd World (when someone gets around to\n"
"implementing it)."
msgstr "" msgstr ""
#: Game.Levels.Algorithm #: Game.Levels.Algorithm
@@ -3150,6 +3154,16 @@ msgid "# Summary\n"
"The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\n" "The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\n"
"truth tables).\n" "truth tables).\n"
"\n" "\n"
"## Details\n"
"\n"
"`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,\n"
"it doesn't even know `add_zero`. The only things that `tauto` knows about numbers\n"
"are firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.\n"
"What `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`\n"
"and another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will\n"
"solve this goal, because to solve that goal you don't need to know any facts\n"
"about inequalities or addition, all you need to know is the rules of logic.\n"
"\n"
"## Example\n" "## Example\n"
"\n" "\n"
"If you have `False` as a hypothesis, then `tauto` will solve\n" "If you have `False` as a hypothesis, then `tauto` will solve\n"
@@ -3172,6 +3186,11 @@ msgid "# Summary\n"
"\n" "\n"
"## Example\n" "## Example\n"
"\n" "\n"
"If you have a hypothesis `h : 0 = 1` then `tauto` will solve the goal, because\n"
"`tauto` knows `0 ≠ 1` and this is enough to prove `False`, which implies any goal.\n"
"\n"
"## Example\n"
"\n"
"If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n" "If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n"
"`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\n" "`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\n"
"If you switch the goal and hypothesis in this example, `tauto` would solve it too." "If you switch the goal and hypothesis in this example, `tauto` would solve it too."
@@ -3230,11 +3249,13 @@ msgid "`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n"
msgstr "" msgstr ""
#: Game.Levels.AdvMultiplication.L05le_mul_right #: Game.Levels.AdvMultiplication.L05le_mul_right
msgid "In Prime Number World we will be proving that $2$ is prime.\n" msgid "One day this game will have a Prime Number World, with a final boss\n"
"of proving that $2$ is prime.\n"
"To do this, we will have to rule out things like $2 = 37 × 42.$\n" "To do this, we will have to rule out things like $2 = 37 × 42.$\n"
"We will do this by proving that any factor of $2$ is at most $2$,\n" "We will do this by proving that any factor of $2$ is at most $2$,\n"
"which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n" "which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
"until it becomes the goal, using pretty much everything which we've proved in this world so far." "until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n"
"`mul_le_mul_right`."
msgstr "" msgstr ""
#: Game.Levels.AdvMultiplication.L05le_mul_right #: Game.Levels.AdvMultiplication.L05le_mul_right
@@ -3366,6 +3387,16 @@ msgid "Now the goal can be deduced from `h2` by pure logic, so use the `tauto`\n
"tactic." "tactic."
msgstr "" msgstr ""
#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "Here's the short proof:\n"
"```\n"
"have h2 := mul_ne_zero a b\n"
"tauto\n"
"```\n"
"This works because, given `mul_ne_zero a b`,\n"
"the argument is reduced to pure logic."
msgstr ""
#: Game.Levels.AdvMultiplication.L09mul_left_cancel #: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "mul_left_cancel" msgid "mul_left_cancel"
msgstr "" msgstr ""