update Game.json
This commit is contained in:
1349
.i18n/zh/Game.json
1349
.i18n/zh/Game.json
File diff suppressed because one or more lines are too long
@@ -5070,39 +5070,3 @@ msgstr ""
|
||||
"在这个游戏中,你将根据皮亚诺公理重新构建自然数集 $\\mathbb{N}$,学习在 Lean 中证明定理的基础知识。\n"
|
||||
"\n"
|
||||
"这是对 Lean 的一个很好的初步介绍!"
|
||||
|
||||
#~ msgid ""
|
||||
#~ "## Summary\n"
|
||||
#~ "\n"
|
||||
#~ "`repeat t` repeatedly applies the tactic `t`\n"
|
||||
#~ "to the goal. You don't need to use this\n"
|
||||
#~ "tactic, it just speeds things up sometimes.\n"
|
||||
#~ "\n"
|
||||
#~ "## Example\n"
|
||||
#~ "\n"
|
||||
#~ "`repeat rw [add_zero]` will turn the goal\n"
|
||||
#~ "`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n"
|
||||
#~ "into the goal\n"
|
||||
#~ "`a = b`.\n"
|
||||
#~ "\"\n"
|
||||
#~ "\n"
|
||||
#~ "TacticDoc nth_rewrite \"\n"
|
||||
#~ msgstr ""
|
||||
#~ "## 小结\n"
|
||||
#~ "\n"
|
||||
#~ "`repeat t` 反复应用策略 `t` 到目标上。这个是个可选策略,它只是有时可以节省步骤。\n"
|
||||
#~ "\n"
|
||||
#~ "## 示例\n"
|
||||
#~ "\n"
|
||||
#~ "`repeat rw [add_zero]` 会将目标\n"
|
||||
#~ "`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n"
|
||||
#~ "变为\n"
|
||||
#~ "`a = b`。\n"
|
||||
#~ "\n"
|
||||
|
||||
#~ msgid ""
|
||||
#~ "\n"
|
||||
#~ "`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$\n"
|
||||
#~ msgstr ""
|
||||
#~ "\n"
|
||||
#~ "`add_left_eq_self x y` 是 $x + y = y\\implies x=0$ 的定理名字。\n"
|
||||
|
||||
Reference in New Issue
Block a user