From c5f6cde8fb77f6a4221e10f520a08599b03136ad Mon Sep 17 00:00:00 2001
From: Oling Cat <olingcat@gmail.com>
Date: Tue, 18 Jun 2024 03:08:12 +0800
Subject: [PATCH] Fix title page

---
 SUMMARY.md                | 16 ++++++++--------
 title_page.md => title.md | 10 +++++-----
 2 files changed, 13 insertions(+), 13 deletions(-)
 rename title_page.md => title.md (69%)

diff --git a/SUMMARY.md b/SUMMARY.md
index 75aa5b1..adc4f86 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -18,19 +18,19 @@
 
 -->
 
-# Lean 4定理证明
+# Lean 4 定理证明
 
-[Lean 4定理证明](title_page.md)
+[Lean 4 定理证明](./title.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)
\ No newline at end of file
+- [公理与计算](./axioms_and_computation.md)
diff --git a/title_page.md b/title.md
similarity index 69%
rename from title_page.md
rename to title.md
index 0f3cbb2..ffce9e1 100644
--- a/title_page.md
+++ b/title.md
@@ -1,10 +1,10 @@
+# Lean 4 定理证明
+
 <!--
 # Theorem Proving in Lean 4
 -->
 
-# 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/)。