From 53676628d8a9b2e0f6e66d812b1b918c09680aa8 Mon Sep 17 00:00:00 2001 From: subfish-zhou Date: Mon, 16 Sep 2024 20:53:39 +0200 Subject: [PATCH] fix ch2 --- lean/main/02_overview.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean/main/02_overview.lean b/lean/main/02_overview.lean index b9f3582..22108ad 100644 --- a/lean/main/02_overview.lean +++ b/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` 上时看到一些输出，这都是反繁饰器的工作。 本书中，您将看到对繁饰器的引用；在「附加内容：美观打印」一章中，您可以阅读有关反繁饰器的内容。