Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.
<1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp in a level, you can use it henceforth in any level.The options are:
": "游戏规则决定是否允许跳过关卡，以及游戏是否允许在证明中使用未解锁的策略和定理。
<1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在另一个关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp，那么你可以在任何关卡中使用它。
选项是：
", + "Lean Game Server": "LEAN 游戏服务器", + "Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.
<1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp in a level, you can use it henceforth in any level.The options are:
": "游戏规则决定是否允许跳过关卡，以及游戏是否只允许在证明中使用已解锁的策略和定理。
<1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在其他关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp，你可以在任何关卡中使用它。选项有：
", "Game Rules": "游戏规则", "levels": "关卡", "tactics": "策略", @@ -20,11 +20,11 @@ "Leave World": "离开世界", "previous level": "上一关", "Previous": "上一关", - "Editor mode is enforced!": "编辑器模式开启！", + "Editor mode is enforced!": "编辑器模式已启用！", "Editor mode": "编辑器模式", "Typewriter mode": "打字机模式", - "information, Impressum, privacy policy": "", - "Preferences": "", + "information, Impressum, privacy policy": "信息、版权说明、隐私政策", + "Preferences": "偏好设置", "Game Info & Credits": "游戏信息和荣誉", "Game Info": "游戏信息", "Clear Progress": "清除进度", @@ -43,14 +43,14 @@ "Current Goal": "当前目标", "Objects": "对象", "Assumptions": "假设", - "Further Goals": "Further Goals", + "Further Goals": "进一步目标", "No Goals": "无目标", - "Loading goal…": "加载目标。。。", - "Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。", - "Waiting for Lean server to start…": "等待 Lean 服务器启动。。。", - "Level completed! 🎉": "完成关卡！🎉", + "Loading goal…": "加载目标中。。。", + "Click somewhere in the Lean file to enable the infoview.": "单击 Lean 文件中的某处以启用信息视图。", + "Waiting for Lean server to start…": "等待 Lean 服务器启动中…", + "Level completed! 🎉": "关卡完成！🎉", "Level completed with warnings 🎭": "关卡完成（带有警告） 🎭", - "Retry proof from here": "从这里重新试着证明", + "Retry proof from here": "从这里重新尝试证明", "Active Goal": "当前目标", "Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：", "Line": "行", @@ -61,34 +61,35 @@ "Theorems": "定理", "Not unlocked yet": "尚未解锁", "Not available in this level": "本关卡不提供", - "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "", - "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "没有加载游戏。使用<1>http://localhost:3000/#/g/local/FOLDER直接从本地文件夹打开游戏。", - "As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.
<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "", - "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.Featured games on this page are added manually. Please get in contact and we'll happily add yours.
": "", - "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "", + "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "这是一个为证明助手 <1>Lean (Lean 4) 及其数学库 <5>mathlib 设计的学习游戏库", + "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "未加载游戏。访问 <1>http://localhost:3000/#/g/local/FOLDER 从本地文件夹打开游戏。", + "As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.
<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "这个服务器部署在我们大学的机器上，运行能力有限，目前估计最多可同时支持约 70 个游戏。我们希望将来能更有效地解决并测试这些限制。
<1>游戏和基础设施的许多方面仍在开发之中。如果您遇到任何问题，欢迎在 <1>GitHub 上提交问题反馈。", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.Featured games on this page are added manually. Please get in contact and we'll happily add yours.
": "<0>如果你打算编写自己的游戏，可以使用 <1>GameSkeleton Github Repo 作为模板，并参阅 <3>如何创建游戏。<1>你可以直接将游戏上传至服务器，并通过正确的 URL 进行游戏。上面的 <1>说明 已详细介绍了如何将游戏加载到服务器的步骤。如果你有任何疑问，请随时联系我们。本页上的精选游戏都是手动添加的。如果你想添加你的游戏，请与我们联系，我们非常欢迎。
", + + "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "此服务器是 Heinrich-Heine-Universität Düsseldorf 项目 <1>ADAM：预见数学的数字时代 的一部分。", "Prerequisites": "前置条件", - "Worlds": "世界(Worlds)", + "Worlds": "世界", "Levels": "关卡", "Language": "语言", - "Development notes": "", - "Adding new games": "", - "Funding": "", - "Do you want to delete your saved progress irreversibly?
(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)
": "您是否想要不可逆转地删除您的游戏进度？
（这将删除您的证明和您收集的定理和策略。其他游戏的进度不会被删除。）
", + "Development notes": "开发笔记", + "Adding new games": "添加新游戏", + "Funding": "资助", + "Do you want to delete your saved progress irreversibly?
(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)
": "您确定要永久删除您的游戏进度吗？
（此操作将删除您的所有证明和收集的定理与策略，但不会影响其他游戏的保存数据。）
", "Delete Progress?": "删除进度？", "Delete": "删除", "Download & Delete": "下载和删除", "Cancel": "取消", "Layout": "布局", "Always visible": "始终可见", - "Save my settings (in the browser store)": "", - "Select a JSON file with the saved game progress to load your progress.
<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "选择一个包含已保存游戏进度的JSON文件来加载您的进度。
<1><0>警告：这将删除您当前的游戏进度！首先考虑<2>下载您当前的进度！", + "Save my settings (in the browser store)": "保存我的设置（在浏览器中存储）", + "Select a JSON file with the saved game progress to load your progress.
<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "选择一个包含已保存游戏进度的 JSON 文件来加载您的进度。
<1><0>警告：这将删除您当前的游戏进度！请考虑先<2>下载您当前的进度！", "Upload Saved Progress": "上传保存的进度", "Load selected file": "加载所选文件", "Mobile": "移动端", "Auto": "自动", "Desktop": "桌面端", - "Level": "", - "Introduction": "", - "Retry": "", - "Failed command": "" + "Level": "关卡", + "Introduction": "介绍", + "Retry": "重试", + "Failed command": "命令失败" }