ch 7

lean/main/05_syntax.lean

@@ -229,7 +229,7 @@ syntax "binCompact(" ("Z" <|> "O"),+ ")" : term --使用括号来组合
 /-
 **可选项**
 
-作为最后一个功能，让我们添加一个可选的字符串注释，用来解释所声明的二进制字面量：
+作为最后一个功能，让我们添加一个可选填的字符串注释，用来解释所声明的二进制字面量：
 -/
 
 -- (...)? 表示括号中的部分是可有可无的

lean/main/06_macros.lean

@@ -147,13 +147,13 @@ macro_rules
 #check cut_tuple (1, 2, 3) -- (2, 3) : Nat × Nat
 
 /-!
-本节的最后一部分将介绍所谓的「反引号拼接」。反引号拼接有两种类型，首先是可选拼接。例如，我们可能会声明一个带有可选参数的语法，比如我们自己的 `let`。（现实例子是，仿写另一种函数式语言中的 `let`）：
+本节的最后一部分将介绍所谓的「反引号拼接」。反引号拼接有两种类型，首先是可选拼接。例如，我们可能会声明一个带有可选填参数的语法，比如我们自己的 `let`。（现实例子是，仿写另一种函数式语言中的 `let`）：
 -/
 
 syntax "mylet " ident (" : " term)? " := " term " in " term : term
 
 /-!
-这里涉及一个可选参数 `(" : " term)?`，用户可以通过它定义左边项的类型。按照我们目前掌握的方法，我们需要编写两个 `macro_rules`，一个处理带可选参数的情况，一个处理不带的情况。然而，语法翻译的其余部分在有无可选参数的情况下完全相同，因此我们可以使用拼接来同时定义两种情况：
+这里涉及一个可选填参数 `(" : " term)?`，用户可以通过它定义左边项的类型。按照我们目前掌握的方法，我们需要编写两个 `macro_rules`，一个处理带可选填参数的情况，一个处理不带的情况。然而，语法翻译的其余部分在有无可选填参数的情况下完全相同，因此我们可以使用拼接来同时定义两种情况：
 -/
 
 macro_rules