ch 4

Lean-zh · Sep 26, 2024 · e3ca7a4 · e3ca7a4
1 parent 17e6541
commit e3ca7a4
Show file tree

Hide file tree

Showing 3 changed files with 161 additions and 344 deletions.
diff --git a/README.md b/README.md
@@ -1,10 +1,13 @@
-# A Lean 4 Metaprogramming Book
+# Lean 4 元编程
 
 Authors: Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat
 
+译者：[subfish_zhou](https://github.com/subfish-zhou)
+
 * The textbook in html format is [here](https://leanprover-community.github.io/lean4-metaprogramming-book/).
+* 中文版网页链接在[这里](https://www.leanprover.cn/mp-lean-zh/)
 
-* A PDF is [available here for download](../../releases/download/latest/Metaprogramming.in.Lean.4.pdf) (and is rebuilt on each change).
+* A PDF is [available here for download](../../releases/download/latest/Metaprogramming.in.Lean.4.pdf) (中文版PDF会乱码).
 
 ## Contributing
 

diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean
@@ -1,6 +1,8 @@
 /-
 # 介绍
 
+本书英文原文：[Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/)
+
 ## 本书的目的
 
 本书的目的是教你 Lean 4 元编程，你将学会：