-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #4 from Lean-zh/type-classes
Type Classes: finished.
- Loading branch information
Showing
4 changed files
with
1,625 additions
and
1,078 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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/)。 |
Oops, something went wrong.