Fix title page

.github/workflows/deploy.yml

@@ -22,8 +22,11 @@ jobs:
       shell: bash
       run: |
         ./mdbook-linux/mdbook build
+        ls -alF ./out/
         rm -rf ./out/.git
         rm -rf ./out/.github
+        echo "# After remove"
+        ls -alF ./out/
     - name: Deploy 🚀
       uses: JamesIves/[email protected]
       with:

SUMMARY.md

@@ -18,19 +18,19 @@
 
 -->
 
-# Lean 4定理证明
+# Lean 4 定理证明
 
-[Lean 4定理证明](title_page.md)
+[Lean 4 定理证明](./index.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 → index.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) 译**
 
@@ -17,5 +17,5 @@ written for Lean 2, and the Lean 3 version is available
 -->
 
 本书假定你使用 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/)。
+中的 [快速开始](https://www.leanprover.cn/lean4/doc/quickstart.html) 一节。
+本书的第一版为 Lean 2 编写，Lean 3 版请访问 [此处](https://leanprover.github.io/theorem_proving_in_lean/)。