Merge pull request #4 from Lean-zh/type-classes

Type Classes: finished.

book.toml

@@ -11,7 +11,7 @@ build-dir = "out"
 
 [output.html]
 # additional-css = ["custom.css", "pygments.css"]
-# additional-js = ["custom.js"]
+additional-js = ["custom.js"]
 mathjax-support = true
 site-url = "/tp-lean-zh/"
 git-repository-url = "https://github.com/Lean-zh/tp-lean-zh"

custom.js

@@ -0,0 +1,7 @@
+const newline = /(?<=[，。、：」）])\n(?!\n)/g;
+const space = /\s+(<.+?>\p{Script=Han}.+?<\/.+?>)\s+/g
+const paras = document.querySelectorAll("#content > main > p");
+for (const p of paras) {
+  p.innerHTML = p.innerHTML.replace(newline, "");
+  p.innerHTML = p.innerHTML.replace(space, "$1");
+}

title_page.md

@@ -1,9 +1,21 @@
-# Theorem Proving in Lean 4
-
-*by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community*
-
-This version of the text assumes you’re using Lean 4. See the
-[Quickstart section](https://lean-lang.org/lean4/doc/quickstart.html) of
-the [Lean 4 Manual](https://lean-lang.org/lean4/doc/) to install Lean. The first version of this book was
-written for Lean 2, and the Lean 3 version is available
-[here](https://leanprover.github.io/theorem_proving_in_lean/).
+<!--
+# Theorem Proving in Lean 4
+-->
+
+# Lean 4 定理证明
+
+作者：*Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community*
+
+**[Lean-zh 项目组](https://github.com/Lean-zh) 译**
+
+<!--
+This version of the text assumes you’re using Lean 4. See the
+[Quickstart section](https://lean-lang.org/lean4/doc/quickstart.html) of
+the [Lean 4 Manual](https://lean-lang.org/lean4/doc/) to install Lean. The first version of this book was
+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/)。