fix ch2

lean/main/02_overview.lean

@@ -55,7 +55,7 @@ Lean 编译过程可以总结为下图：
 
 这些定义并不相互排斥。此处定义繁饰是将 `Syntax` 转换为 `Expr`，只是为了实现这种转换，我们需要很多技巧。我们需要推断隐式参数、实例化元变量、执行统一、解析标识符等。其他地方只是把这些繁饰操作的一部分也称为繁饰。
 
-在 Lean 中，还存在一个与繁饰相反的反繁饰（delaboration）过程。在反繁饰过程中，一个 `Syntax` 被转换成一个 `Expr` 对象；然后格式化程序将其转换成一个 `Format` 对象，该对象可以在 Lean 的信息视图中显示。每次您将某些内容记录到屏幕上，或者将鼠标悬停在 `#check` 上时看到一些输出，这都是反繁饰器的工作。
+在 Lean 中，还存在一个与繁饰相反的反繁饰（delaboration）过程。在反繁饰过程中，一个 `Expr` 被转换成一个 `Syntax` 对象；然后格式化程序将其转换成一个 `Format` 对象，该对象可以在 Lean 的信息视图中显示。每次您将某些内容记录到屏幕上，或者将鼠标悬停在 `#check` 上时看到一些输出，这都是反繁饰器的工作。
 
 本书中，您将看到对繁饰器的引用；在「附加内容：美观打印」一章中，您可以阅读有关反繁饰器的内容。