Update

.gitignore

@@ -2,3 +2,4 @@ build/
 lake-packages/
 .lake/
 **/.DS_Store
+.i18n/*.mo

.i18n/Game-zh_CN.po

@@ -294,7 +294,7 @@ msgstr ""
 "\n"
 "* 需要方括号。`rw h` 永远不会正确。\n"
 "\n"
-"* 如果 `h` 不是一个 *equality* 的 *proof* （形式为 `A = B` 的语句）、\n"
+"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的语句）、\n"
 "例如，如果 `h` 是一个函数或蕴涵、\n"
 "那么 `rw` 就不是您要使用的策略。例如\n"
 "`rw [P = Q]` 绝对不正确：`P = Q` 是定理*陈述、\n"
@@ -302,8 +302,8 @@ msgstr ""
 "\n"
 "## 详情\n"
 "\n"
-"`rw` 战术是 \"代入 \"的一种方法。有\n"
+"`rw` 策略是 \"代入 \"的一种方法。有\n"
-"有两种不同的情况可以使用这种战术。\n"
+"有两种不同的情况可以使用这种策略。\n"
 "\n"
 "1) 基本用法：如果 `h : A = B` 是一个假设或\n"
 "如果目标包含一个或多个 `A`s，那么 `rw [h]`\n"
@@ -645,7 +645,7 @@ msgid ""
 msgstr ""
 "`add_zero a` 是 `a + 0 = a` 的证明。\n"
 "\n"
-"## 总结\n"
+"## 小结\n"
 "\n"
 "`add_zero` 实际上是一个函数，它接受一个数字，并返回关于那个数字的定理的证明。例如，`add_zero 37` 是 `37 + 0 = 37` 的证明。\n"
 "\n"
@@ -670,7 +670,7 @@ msgid ""
 "into the goal\n"
 "`a = b`."
 msgstr ""
-"## 总结\n"
+"## 小结\n"
 "\n"
 "`repeat t` 会重复应用策略 `t` 到目标上。你不一定要使用这个策略，它有时只是加快了速度。\n"
 "\n"
@@ -3435,7 +3435,7 @@ msgid ""
 "\n"
 "`a = b`."
 msgstr ""
-"# 总结\n"
+"# 小结\n"
 "\n"
 "如果你有一个假设\n"
 "\n"
@@ -4379,7 +4379,7 @@ msgstr ""
 
 #: Game.Levels.LessOrEqual.L07or_symm
 msgid "This time, use the `left` tactic."
-msgstr "这一次，使用 `left` 战术。"
+msgstr "这一次，使用 `left` 策略。"
 
 #: Game.Levels.LessOrEqual.L07or_symm
 msgid ""