catch up with the latest

lean/main/01_intro.lean

@@ -32,7 +32,7 @@
 
 在大多数系统中，元层面活动是用与我们当前用来编写代码的语言不同的语言完成的。在Isabelle中，元层面语言是ML和Scala。在Coq中，它是OCaml。在Agda中，是Haskell。在 Lean 4 中，元代码主要是用 Lean 本身编写的，还有一些用C++编写的组件。
 
-Lean 的一个很酷且方便的地方是，它允许我们用日常在对象层面写 Lean 的方式自定义句法节点，并实现元层面例程。例如，可以编写符号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为[**反射**](https://zh.wikipedia.org/wiki/%E5%8F%8D%E5%B0%84%E5%BC%8F%E7%BC%96%E7%A8%8B)。我们可以说，在Lean中，元层面被「反射」到对象层面。
+Lean 的一个很酷且方便的地方是，它允许我们用日常在对象层面写 Lean 的方式自定义句法节点，并实现元层面例程。例如，可以编写记号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为[**反射**](https://zh.wikipedia.org/wiki/%E5%8F%8D%E5%B0%84%E5%BC%8F%E7%BC%96%E7%A8%8B)。我们可以说，在Lean中，元层面被「反射」到对象层面。
 
 用Ruby、Python或Javascript等语言做元编程的方式可能是使用预定义的元编程方法来即时定义一些东西。例如，在Ruby中你可以使用 `Class.new` 和 `define_method` 用于在程序执行时即时定义一个新类及其新方法（其中包含新代码！）。
 

lean/main/02_overview.lean

@@ -98,7 +98,7 @@ elab 函数也可以是不同的类型，例如用于实现 `#help` 的 `Command
 
 上面是这三个基本命令的执行流程，现在明确地阐述一下。执行顺序遵循以下伪代码模板：`syntax (macro; syntax)* elab`。
 
-考虑以下示例。
+考虑以下示例。（我们将在后面的章节详细解释具体语法）
 -/
 import Lean
 open Lean Elab Command

lean/main/03_expressions.lean

@@ -85,9 +85,11 @@ set_option pp.universes true in
 
 ## 构造表达式
 
-我们可以构造的最简单的表达式是常量。我们使用 `const` 构造器并为其指定一个名称和一个宇宙等级列表。我们的大多数示例仅涉及非宇宙多态常量，在这种情况下列表为空。
+### 常量
 
-我们还展示了第二种形式，其中我们用双反引号写名称。这可以检查名称是否真的引用了已定义的常量，有助于避免拼写错误。
+我们可以构造的最简单的表达式是常量。我们使用 `const` 构造器并为其指定一个名称和一个宇宙等级列表。我们的大多数示例仅涉及非宇宙多态常量，在这种情况下宇宙等级列表为空。
+
+反引号 「\`」 标识 `Name` 类型的项，也就是一个名称。名称可以任取，但有时你需要引用已定义的常量，此时可以用双反引号写名称。双反引号可以检查名称是否真的引用了已定义的常量，有助于避免拼写错误。
 -/
 
 open Lean
@@ -99,7 +101,7 @@ def z := Expr.const ``Nat.zero []
 #eval z -- Lean.Expr.const `Nat.zero []
 
 /-
-双反引号变体还可以解析给定的名称，使其完全合规。为了说明这种机制，下面还有两个例子。第一个表达式 `z₁` 是不安全的：如果我们在 `Nat` 命名空间未开放的上下文中使用它，Lean 会抱怨环境中没有名为 `zero` 的常量。相比之下，第二个表达式 `z₂` 包含完全合格的名称 `Nat.zero`，不存在这个问题。
+双反引号还可以解析给定的名称。下例演示了这种机制。第一个表达式 `z₁` 是不安全的：如果我们在 `Nat` 命名空间未开放的上下文中使用它，Lean 会抱怨环境中没有名为 `zero` 的常量。相比之下，第二个表达式 `z₂` 包含已有的名称 `Nat.zero`，不存在这个问题。
 -/
 
 open Nat
@@ -111,12 +113,14 @@ def z₂ := Expr.const ``zero []
 #eval z₂ -- Lean.Expr.const `Nat.zero []
 
 /-
-我们考虑的下一类表达式是函数应用。这些可以使用 `app` 构造器构建，其中第一个参数是函数的表达式，第二个参数是参数的表达式。
+### 函数应用
+
+我们考虑的下一类表达式是函数应用。这些可以使用 `app` 构造器构建，其中第一个参数是函数表达式，第二个参数是表示函数的参数的表达式。
 
 以下是两个示例。第一个只是将一个常量应用于另一个常量。第二个是递归定义，给出一个作为自然数函数的表达式。
 -/
 
-def one := Expr.app (.const ``Nat.succ []) z
+def one := Expr.app (.const ``Nat.succ []) z -- Expr.const可以省略为.const
 #eval one
 -- Lean.Expr.app (Lean.Expr.const `Nat.succ []) (Lean.Expr.const `Nat.zero [])
 
@@ -134,6 +138,8 @@ def sumExpr : Nat → Nat → Expr
 /-
 最后两个函数的 `#eval` 输出表达式非常大，您可以自己试试看。
 
+### lambda 抽象
+
 接下来，我们使用构造器 `lam` 来构造一个简单的函数，该函数接受任何自然数 `x` 并返回 `Nat.zero`。参数 `BinderInfo.default` 表示 `x` 是一个显式参数（而不是隐式或类型类参数）。
 -/
 
@@ -171,7 +177,7 @@ elab "mapAddOneNil" : term => return mapAddOneNil
 set_option pp.universes true in
 set_option pp.explicit true in
 #check mapAddOneNil
--- @List.map.{1, 1} Nat Nat (fun x => Nat.add x 1) (@List.nil.{1} Nat) : List.{1} Nat
+-- @List.map.{0, 0} Nat Nat (fun x => x.add 1) (@List.nil.{0} Nat) : List.{0} Nat
 
 #reduce mapAddOneNil
 -- []

lean/main/06_macros.lean

@@ -125,7 +125,7 @@ it will be essential to all non trivial things that are syntax related.
 First things first we call the `` `() `` syntax a `Syntax` quotation.
 When we plug variables into a syntax quotation like this: `` `($x) ``
 we call the `$x` part an anti-quotation. When we insert `x` like this
-it is required that `x` is of type `TSyntax x` where `x` is some `Name`
+it is required that `x` is of type `TSyntax y` where `y` is some `Name`
 of a syntax category. The Lean compiler is actually smart enough to figure
 the syntax categories that are allowed in this place out. Hence you might
 sometimes see errors of the form:
@@ -161,7 +161,7 @@ the function is receiving is a numeric literal and can thus naturally
 be converted to a `Nat`.
 
 If we use the antiquotation syntax in pattern matching it will, as discussed
-in the syntax chapter, give us a a variable `x` of type `` TSyntax y `` where
+in the syntax chapter, give us a variable `x` of type `` TSyntax y `` where
 `y` is the `Name` of the syntax category that fits in the spot where we pattern matched.
 If we wish to insert a literal `$x` into the `Syntax` for some reason,
 for example macro creating macros, we can escape the anti quotation using: `` `($$x) ``.

lean/main/09_tactics.lean

@@ -55,13 +55,13 @@ example : 42 = 42 := by
 We can now try a harder problem, that cannot be immediately dispatched by `rfl`:
 -/
 
-#check_failure (by custom_tactic : 42 = 43 ∧ 42 = 42)
+#check_failure (by custom_tactic : 43 = 43 ∧ 42 = 42)
 -- type mismatch
 --   Iff.rfl
 -- has type
 --   ?m.1437 ↔ ?m.1437 : Prop
 -- but is expected to have type
---   42 = 43 ∧ 42 = 42 : Prop
+--   43 = 43 ∧ 42 = 42 : Prop
 
 /-
 We extend the `custom_tactic` tactic with a tactic that tries to break `And`