Merge pull request #1 from subfish-zhou/master

lean/main/01_intro.lean

@@ -1,23 +1,34 @@
 /-
-# Introduction
+-- # Introduction
 
-## What's the goal of this book?
+-- ## What's the goal of this book?
 
-This book aims to build up enough knowledge about metaprogramming in Lean 4 so
-you can be comfortable enough to:
+-- This book aims to build up enough knowledge about metaprogramming in Lean 4 so
+-- you can be comfortable enough to:
 
-* Start building your own meta helpers (defining new Lean notation such as `∑`,
-building new Lean commands such as `#check`, writing tactics such as `use`, etc.)
-* Read and discuss metaprogramming APIs like the ones in Lean 4 core and
-Mathlib4
+-- * Start building your own meta helpers (defining new Lean notation such as `∑`,
+-- building new Lean commands such as `#check`, writing tactics such as `use`, etc.)
+-- * Read and discuss metaprogramming APIs like the ones in Lean 4 core and
+-- Mathlib4
 
-We by no means intend to provide an exhaustive exploration/explanation of the
-entire Lean 4 metaprogramming API. We also don't cover the topic of monadic
-programming in Lean 4. However, we hope that the examples provided will be
-simple enough for the reader to follow and comprehend without a super deep
-understanding of monadic programming. The book
-[Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/)
-is a highly recommended source on that subject.
+-- We by no means intend to provide an exhaustive exploration/explanation of the
+-- entire Lean 4 metaprogramming API. We also don't cover the topic of monadic
+-- programming in Lean 4. However, we hope that the examples provided will be
+-- simple enough for the reader to follow and comprehend without a super deep
+-- understanding of monadic programming. The book
+-- [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/)
+-- is a highly recommended source on that subject.
+
+# 介绍
+
+## 本书的目的
+
+本书的目的是在 Lean 4 中建立足够的元编程知识，你将学会：
+
+- 构建自己的元助手（定义新的 Lean 符号，如「∑」，构建新的 Lean 命令，如`#check`，编写策略，如`use`等）
+- 阅读和讨论元编程API，如Lean 4 core和Mathlib4中的API
+
+我们绝不打算对整个 Lean 4 元编程API进行详尽的解释。我们也不涉及单子（Monad）化编程的主题。我们希望示例足够简单，不太熟悉单子化编程也能跟上。强烈推荐[ Lean 中的函数式编程](https://www.leanprover.cn/fp-lean-zh/)作为这个主题的参考。
 
 ## Book structure
 

md/SUMMARY.md

@@ -1,32 +1,32 @@
-# Summary
+# 目录
 
-# Main
+# 正文
 
-- [Introduction](./main/01_intro.md)
-- [Overview](./main/02_overview.md)
-- [Expressions](./main/03_expressions.md)
+- [介绍](./main/01_intro.md)
+- [概述](./main/02_overview.md)
+- [表达式](./main/03_expressions.md)
 - [MetaM](./main/04_metam.md)
-- [Syntax](./main/05_syntax.md)
-- [Macros](./main/06_macros.md)
-- [Elaboration](./main/07_elaboration.md)
-- [Embedding DSLs By Elaboration](./main/08_dsls.md)
-- [Tactics](./main/09_tactics.md)
-- [Lean4 Cheat-sheet](./main/10_cheat-sheet.md)
+- [句法](./main/05_syntax.md)
+- [宏](./main/06_macros.md)
+- [繁饰](./main/07_elaboration.md)
+- [通过繁饰嵌入DSL](./main/08_dsls.md)
+- [证明策略](./main/09_tactics.md)
+- [Lean4速查表](./main/10_cheat-sheet.md)
 
-# Extra
+# 额外内容
 
-- [Options](./extra/01_options.md)
+- [选项](./extra/01_options.md)
 <!-- - [Attributes]() -->
-- [Pretty Printing](./extra/03_pretty-printing.md)
+- [美观打印](./extra/03_pretty-printing.md)
 
-# Solutions
+# 习题解答
 
 <!-- - [Introduction]() -->
 <!-- - [Overview]() -->
-- [Expressions](./solutions/03_expressions.md)
+- [表达式](./solutions/03_expressions.md)
 - [`MetaM`](./solutions/04_metam.md)
-- [`Syntax`](./solutions/05_syntax.md)
+- [句法](./solutions/05_syntax.md)
 <!-- - [Macros]() -->
-- [Elaboration](./solutions/07_elaboration.md)
+- [繁饰](./solutions/07_elaboration.md)
 <!-- - [DSLs]() -->
-- [Tactics](./solutions/09_tactics.md)
+- [证明策略](./solutions/09_tactics.md)