Lean 的设计目标是交互式使用，而不是采用批处理模式——在这种模式下，整个文件被一次性输入，再被转换为目标代码或错误消息。
许多为交互式使用而设计的编程语言都提供 REPL，它是 “R（读取）-E（求值）-P（打印）-L（循环）”的缩写，因为代码会被解析（“读取”）、求值并显示结果，而且这一过程可以按需重复任意多次。用户可以在其中输入并测试代码，也可以使用命令加载源文件、检查项的类型或查询环境。
Lean 的交互功能基于另一种范式。
Lean 并不在程序之外提供单独的命令提示符，而是在源文件的上下文中提供 命令来完成相同的任务。
依照惯例，供交互使用、而非作为持久代码制品一部分的命令，都以 # 为前缀。
3.1. 对项求值🔗
Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 命令用于将代码作为程序运行。
具体而言，它能够执行 IO 动作，采用按值调用的求值策略，会执行 partial 函数，并且类型与证明都会被擦除。
若要改用属于定义相等一部分的归约规则来归约项，请使用 Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)` and `(types := true)` to reduce them.
Recall that propositions are types in Lean.
**Warning:** This can be a computationally expensive operation,
especially for complex expressions.
Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
#reduce。
语法对项求值
command ::= ...
| `#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
command ::= ...
| `#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval e 会编译表达式 e、运行编译后的代码并打印结果值。
#eval 的能力会随所导入内容而平稳降级。导入 Lean.Elab.Command 模块可获得完整能力。
出于可靠性考虑，#eval 拒绝求值直接或间接依赖 sorry 的表达式，因为 sorry
可能导致运行时不稳定或崩溃。可使用 #eval! e 命令越过此检查。
选项：
另见：使用 #reduce e 通过项归约进行求值。
Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 总会先由 Lean 的精译器精译所提供的项，再进行编译。
随后，它会检查该项是否传递依赖于任何 sorry；若存在此类依赖，除非以 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval! 形式调用命令，否则求值将终止。
这是因为编译后的代码可能依赖编译期不变量（例如数组查找不能越界），而这些不变量由适当命题的证明保证；运行包含不完整证明的代码（或使用 sorry“证明”错误命题的代码）可能导致 Lean 自身崩溃。
代码的运行方式取决于其类型：
-
如果类型位于 IO 单子中，则会在捕获标准输出与标准错误并将其重定向到 Lean 消息日志的上下文中执行。
如果返回值的类型不是 Unit，则会像显示非单子表达式的结果那样显示它。
-
如果类型位于 Lean 内部的某个元编程单子中（CommandElabM、TermElabM、MetaM 或 CoreM），则会在当前上下文中运行。
例如，环境会包含调用 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 之处位于作用域内的定义。
与 IO 一样，所得值会像非单子表达式的结果那样显示。
当 Lean 在 Lake 下运行时，其工作目录（因而也是 IO 动作的工作目录）是当前工作区。
-
如果类型位于其他某个单子 m 中，并且存在 MonadLiftT m CommandElabM 或 MonadEvalT m CommandElabM 实例，则会使用 MonadLiftT.monadLift 或 MonadEvalT.monadEval 将该单子转换为可由 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 运行的单子，之后照常运行。
-
如果项的类型不位于任何受支持的单子中，则将它视为纯值。
编译后的代码会被运行，并显示结果。
精译 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 中的项所产生的辅助定义或其他环境修改都会被丢弃。
如果该项是元编程单子中的动作，那么运行此单子动作对环境所做的更改会被保留。
在模块中使用时，Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 会揭示 Lean 语言服务器与 Lean 编译器处理文件方式之间的差异。
由于 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 会在编译期运行代码，因此要求其代码在元阶段可用。
为便于对模块进行实验，语言服务器会让所有已导入模块在元阶段可用，而编译器则严格遵守 Lean.Parser.Module.importmeta 声明。
因此，使用 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 与 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 嵌入轻量测试的模块，可能在语言服务器中精译成功，却在构建期间失败。
要修复此问题，可以在包含测试的模块中使用 Lean.Parser.Module.importmeta import 导入这些定义：
求值与元阶段
Eval.leanmodule
import Eval.Even
❌️ Docstring on `#guard_msgs` does not match generated message:
- info: [true, false]
+ error: Invalid `meta` definition `_eval`, `isEven` is not accessible here; consider adding `public meta import Eval.Even`
#guard_msgs in
Invalid `meta` definition `_eval`, `isEven` is not accessible here; consider adding `public meta import Eval.Even`#eval [isEven 4, isEven 5]
❌️ Docstring on `#guard_msgs` does not match generated message:
- info: [true, false]
+ error: Invalid `meta` definition `_eval`, `isEven` is not accessible here; consider adding `public meta import Eval.Even`
将 isEven 导入元阶段即可修复此问题：
如果存在相应实例，结果会使用 ToExpr、ToString 或 Repr 实例显示。
如果不存在，而 eval.derive.repr 为 true，Lean 会尝试派生合适的 Repr 实例。
如果既找不到也无法派生合适的实例，就会报错。
将 eval.pp 设为 false，可禁止 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 使用 ToExpr 实例。
显示输出
Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 无法显示函数：
Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
Nat → Nat#eval fun x => x + 1
Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
Nat → Nat
它能够派生实例，以显示没有 ToString 或 Repr 实例的输出：
inductive Quadrant where
| nw | sw | se | ne
Quadrant.nw#eval Quadrant.nw
Quadrant.nw
派生出的实例不会被保存。
禁用 eval.derive.repr 会导致 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 失败：
set_option eval.derive.repr false
Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
Quadrant#eval Quadrant.nw
Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
Quadrant
🔗选项eval.pp
默认值：true
启用后（默认），#eval 会尝试使用 ToExpr 实例，以便用通常的美化打印器输出结果；
禁用后则使用 Repr 或 ToString 实例。
🔗选项eval.type
默认值：false
启用后（默认为禁用），#eval 会美化打印求值结果的类型。
🔗选项eval.derive.repr
默认值：true
启用后（默认），#eval 会在没有其他输出方式时尝试自动派生 Repr 实例。
为单子定义合适的 MonadLift关于提升单子的章节介绍了 MonadLift。或 MonadEval 实例，即可使其能够在 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 中执行。
正如 MonadLiftT 是 MonadLift 实例的传递闭包，MonadEvalT 也是 MonadEval 实例的传递闭包。
与 MonadLiftT 一样，用户不应直接定义额外的 MonadEvalT 实例。
🔗类型类
MonadEval 的传递闭包。
方法
monadEval : {α : Type u} → m α → n α
3.2. 归约项🔗
Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)` and `(types := true)` to reduce them.
Recall that propositions are types in Lean.
**Warning:** This can be a computationally expensive operation,
especially for complex expressions.
Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
#reduce 命令会反复对项应用归约，直到无法再归约为止。
归约会在绑定器下进行；但为避免意外的性能下降，除非启用了 Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)` and `(types := true)` to reduce them.
Recall that propositions are types in Lean.
**Warning:** This can be a computationally expensive operation,
especially for complex expressions.
Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
#reduce 的相应选项，否则会跳过证明和类型。
与 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 命令不同，归约不能产生副作用，并且结果会显示为项，而不是通过 ToString 或 Repr 实例显示。
一般而言，Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)` and `(types := true)` to reduce them.
Recall that propositions are types in Lean.
**Warning:** This can be a computationally expensive operation,
especially for complex expressions.
Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
#reduce 主要用于诊断定义相等与证明项方面的问题，而 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 更适合计算项的值。
尤其是，使用良基递归定义或定义为部分不动点的函数，使用归约引擎计算时要么非常缓慢，要么根本不会归约。
语法归约项
command ::= ...
| `#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)` and `(types := true)` to reduce them.
Recall that propositions are types in Lean.
**Warning:** This can be a computationally expensive operation,
especially for complex expressions.
Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
Configuration for the `#reduce` command.
#reduce <expression> 将表达式 <expression> 归约至范式，即持续应用归约规则，
直到无法继续归约。
默认不归约表达式中的证明和类型。使用修饰项 (proofs := true) 和
(types := true) 可分别归约它们。请注意，在 Lean 中命题也是类型。
**警告：**这一操作的计算开销可能很大，复杂表达式尤其如此。
对表达式进行简单求值或执行时，请考虑使用 #eval <expression>。
归约函数
归约一个项会得到它在 Lean 逻辑中的范式。
由于底层项先被归约再显示，因此不需要 ToString 或 Repr 实例。
函数也可以像其他任何项一样显示。
在某些情况下，此范式很短，并且类似于人会编写的项：
fun x => x.succ#reduce (fun x => x + 1)
fun x => x.succ
在另一些情况下，则会暴露诸如加法这类函数被精译到 Lean 核心逻辑中的细节，参见函数的精译：
fun x => (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) x).1 1#reduce (fun x => 1 + x)
fun x => (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) x).1 1
3.6. 使用 #guard_msgs 测试输出🔗
Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令可用于确保某条命令输出的消息符合预期。
配合本节中的交互命令，可以构造一个仅在输出符合预期时才会精译成功的文件；这样的文件可在 Lake 中用作测试驱动程序。
语法记录预期输出
command ::= ...
| `/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.
A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
/-- ... -/ #guard_msgs in cmd 捕获命令 cmd 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
#guard_msgs in
example : α := x
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
或只选择错误：
#guard_msgs(error) in
declaration uses `sorry`example : α := sorry
在上一个示例中，因为警告未被捕获，sorry 上仍会产生警告。可用下述写法彻底丢弃警告：
#guard_msgs(error, drop warning) in
example : α := sorry
一般而言，#guard_msgs 接受一组置于圆括号内、以逗号分隔的配置子句：
#guard_msgs (
默认配置列表为
(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)。
消息过滤器按严重程度选择消息：
过滤器可带有指定操作的前缀：
-
check（默认）：捕获并检查消息；
-
drop：丢弃消息；
-
pass：让消息继续传递。
若未指定过滤器，则假定为 check all。否则从左至右处理这些过滤器，并在末尾隐式
添加 pass all。
空白处理（先去除开头和末尾的空白）：
-
whitespace := exact 要求空白完全匹配；
-
whitespace := normalized 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
-
whitespace := lax 在匹配前把连续空白压缩为一个空格。
消息排序：
位置信息：
子串匹配：
稳定输出：
消息含有自动生成的名称（例如元变量 ?m.47）时，输出可能随运行或 Lean 版本而变化。
使用 set_option pp.mvars.anonymous false 可把匿名元变量替换为 ?_，同时保留
?a 等用户命名的元变量。也可使用 set_option pp.mvars false 把所有元变量替换为
?_。类似地，set_option pp.fvars.anonymous false 会把 _fvar.22 之类的
松散自由变量名替换为 _fvar._。
例如，#guard_msgs (error, drop all) in cmd 表示检查错误并丢弃其他一切消息。
命令精译器对 #guard_msgs 的代码检查有特殊支持。#guard_msgs 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 #guard_msgs 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 #guard_msgs 时，顶层命令精译器才运行代码检查器。
测试返回值
Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令可以确保一组测试用例通过：
def reverse : List α → List α := helper []
where
helper acc
| [] => acc
| x :: xs => helper (x :: acc) xs
#guard_msgs in
#eval reverse ([] : List Nat)
#guard_msgs in
#eval reverse "abc".toList
Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令的行为可通过三种方式指定：
-
提供筛选器，选择要检查的消息子集
-
指定空白字符比较策略
-
决定按消息内容排序，还是按消息产生的顺序排序
这些配置选项写在圆括号中，并以逗号分隔。
语法指定 #guard_msgs 的行为
guardMsgsSpecElt ::=
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
guardMsgsSpecElt ::= ...
| Whitespace handling for `#guard_msgs`:
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
(the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
In all cases, leading and trailing whitespace is trimmed before matching.
guardMsgsSpecElt ::= ...
| Message ordering for `#guard_msgs`:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
This helps with testing commands that are non-deterministic in their ordering.
Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 有三类选项：筛选器、空白字符比较策略和排序方式。
语法#guard_msgs 的输出筛选器
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
#guard_msgs 的消息过滤器规范。
过滤器可带有下列前缀：
-
check（默认）：捕获并检查消息；
-
drop：丢弃消息；
-
pass：让消息继续传递。
若未指定过滤器，则假定为 check all。否则从左至右处理这些过滤器，并在末尾隐式
添加 pass all。
语法#guard_msgs 的空白字符比较
guardMsgsWhitespaceArg ::=
exactguardMsgsWhitespaceArg ::= ...
| laxguardMsgsWhitespaceArg ::= ...
| normalized
比较消息时，始终忽略开头和结尾的空白字符。在此基础上，还可使用以下设置：
-
whitespace := exact 要求空白字符完全匹配。
-
whitespace := normalized 在匹配前将所有换行符转换为空格（默认设置）。这样便可将长行断行。
-
whitespace := lax 在匹配前将连续空白字符折叠为一个空格。
选项 guard_msgs.diff 控制当预期消息与实际产生的消息不匹配时，Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 所产生错误消息的内容。
默认情况下，Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 会逐行显示差异：行首的 + 表示来自实际产生的消息的行，行首的 - 表示来自预期消息的行。
当消息很大而差异很小时，这有助于发现差异所在。
将 guard_msgs.diff 设为 false 后，Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 将只显示实际产生的消息，可将它与源文件中的预期消息进行比较。
如果消息之间的差异令人困惑或信息过载，这样做会比较方便。
🔗选项guard_msgs.diff
默认值：true
启用后（默认），如果预期消息与实际消息不匹配，#guard_msgs 会显示二者的差异；
禁用后则显示实际消息。
显示差异
Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令可用于测试玫瑰树 Tree 的定义，以及创建这种树的函数 Tree.big：
inductive Tree (α : Type u) : Type u where
| val : α → Tree α
| branches : List (Tree α) → Tree α
def Tree.big (n : Nat) : Tree Nat :=
if n < 5 then .branches [.val n, .val (n - 1), .val n, .val (n - 2)]
else .branches [.big (n / 2), .big (n / 3)]
然而，当输出很大时，可能很难看出测试失败源自何处：
set_option guard_msgs.diff false
❌️ Docstring on `#guard_msgs` does not match generated message:
info: Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]#guard_msgs in
Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]#eval Tree.big 20
求值产生：
Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]
禁用 guard_msgs.diff 时，Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令会报告以下错误：
❌️ Docstring on `#guard_msgs` does not match generated message:
info: Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]
启用 guard_msgs.diff 后，差异会被突出显示，使错误更加明显：
set_option guard_msgs.diff true in
❌️ Docstring on `#guard_msgs` does not match generated message:
info: Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
- Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0,
+ Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]
#guard_msgs in
Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]#eval Tree.big 20
❌️ Docstring on `#guard_msgs` does not match generated message:
info: Tree.branches
[Tree.branches
[Tree.branches
[Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0],
- Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0,
+ Tree.branches [Tree.val 1, Tree.val 0, Tree.val 1, Tree.val 0]],
Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1]],
Tree.branches
[Tree.branches [Tree.val 3, Tree.val 2, Tree.val 3, Tree.val 1],
Tree.branches [Tree.val 2, Tree.val 1, Tree.val 2, Tree.val 0]]]
