Fix title page

.github/workflows/deploy.yml

@@ -14,7 +14,7 @@ jobs:
     - name: Download mdbook for Lean
       shell: bash
       run: |
-        curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.6/mdbook-linux.tar.gz
+        curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.15l2/mdbook-linux.tar.gz
         tar xvf mdbook-linux.tar.gz
         ./mdbook-linux/mdbook --help
         ldd ./mdbook-linux/mdbook

SUMMARY.md

@@ -18,19 +18,19 @@
 
 -->
 
-# Lean 4定理证明
+# Lean 4 定理证明
 
-[Lean 4定理证明](title_page.md)
+[Lean 4 定理证明](./title_page.md)
 
 - [介绍](./introduction.md)
 - [依值类型论](./dependent_type_theory.md)
-- [命题和证明](./propositions_and_proofs.md)
+- [命题与证明](./propositions_and_proofs.md)
 - [量词与等价](./quantifiers_and_equality.md)
 - [证明策略](./tactics.md)
-- [与Lean交互](./interacting_with_lean.md)
+- [与 Lean 交互](./interacting_with_lean.md)
 - [归纳类型](./inductive_types.md)
-- [Induction and Recursion](./induction_and_recursion.md)
-- [结构体和记录](./structures_and_records.md)
-- [Type Classes](./type_classes.md)
+- [归纳与递归](./induction_and_recursion.md)
+- [结构体与记录](./structures_and_records.md)
+- [类型类](./type_classes.md)
 - [转换策略模式](./conv.md)
-- [Axioms and Computation](./axioms_and_computation.md)
+- [公理与计算](./axioms_and_computation.md)

title_page.md

@@ -4,7 +4,7 @@
 
 # Lean 4 定理证明
 
-作者：*Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community*
+作者：*Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, 以及来自 Lean 社区的贡献者*
 
 **[Lean-zh 项目组](https://github.com/Lean-zh) 译**
 
@@ -16,6 +16,6 @@ written for Lean 2, and the Lean 3 version is available
 [here](https://leanprover.github.io/theorem_proving_in_lean/).
 -->
 
-本书假定你使用 Lean 4。安装方式参见 [Lean 4 手册](https://www.leanprover.cn/lean4/lean4/doc/)
-中的[快速开始](https://www.leanprover.cn/lean4/doc/quickstart.html)一节。
-本书的第一版为 Lean 2 编写，Lean 3 版请访问[此处](https://leanprover.github.io/theorem_proving_in_lean/)。
+本书假定你使用 Lean 4。安装方式参见 [Lean 4 手册](https://www.leanprover.cn/lean4/doc/)
+中的 [快速开始](https://www.leanprover.cn/lean4/doc/quickstart.html) 一节。
+本书的第一版为 Lean 2 编写，Lean 3 版请访问 [此处](https://leanprover.github.io/theorem_proving_in_lean/)。