3. 与 Lean 交互🔗

Lean 专为交互式使用而设计，而不是作为批处理模式系统，在批处理模式系统中将整个文件输入然后转换为目标代码或错误消息。许多设计用于交互式使用的编程语言都提供 REPL、“Read-Eval-Print Loop” 的缩写；代码会被解析（“read”）、求值并显示结果，此过程可按需重复。可在其中输入和测试代码，并使用加载源文件、类型检查术语或查询环境的命令。 Lean 的交互功能基于不同的范例。 Lean 提供了命令，用于在源文件上下文中完成相同的任务，而不是在程序外部提供单独的命令提示符。按照惯例，用于交互使用而不是作为持久代码工件的一部分的命令以 # 为前缀。

Lean 命令的信息可在 message log 中获取，它累积来自精化器的输出。消息日志中的每个条目都与特定的源范围相关联，并具有 severity。共有三种严重性：information 用于不指示问题的消息，warning 指示潜在问题，error 指示明确问题。对于交互式命令，结果通常作为与命令的前导关键字关联的信息性消息返回。

3.1. 评估条款🔗

syntaxEvaluating Terms

command ::= ...
    | `#eval e` evaluates the expression `e` by compiling and evaluating it.

* 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 term

command ::= ...
    | `#eval e` evaluates the expression `e` by compiling and evaluating it.

* 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! term

#eval e evaluates the expression e by compiling and evaluating it.

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.

Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 元编程 monad（CommandElabM、TermElabM、MetaM 或 CoreM）之一中，则它在当前上下文中运行。例如，环境将包含调用 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 操作的工作目录）是当前的 workspace。
如果该类型位于其他某个单子 m 中，并且存在 MonadLiftT m CommandElabM 或 MonadEvalT m CommandElabM 实例，则使用 MonadLiftT.monadLift 或 MonadEvalT.monadEval 将单子转换为可以与 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 一起运行的单子，然后照常运行。
如果该术语的类型不在任何受支持的 monad 中，则将其视为纯值。运行编译后的代码，并显示结果。

由于详细精化Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 中的术语而产生的辅助定义或其他环境修改将被丢弃。如果该术语是元编程单子中的操作，则通过运行单子操作对环境所做的更改将被保留。

在 module 中使用时，Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 and evaluating it. * 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` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 与 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 导入定义：

Evaluation and Meta

Eval/Even.lean

module
public section
def isEven (n : Nat) : Bool :=
  n % 2 = 0

Eval.lean

module
import Eval.Even

/-- info: [true, false] -/
❌️ 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 导入元阶段修复了问题：

Eval/Even.lean

module
public section
def isEven (n : Nat) : Bool :=
  n % 2 = 0

Eval.lean

module
meta import Eval.Even

/-- info: [true, false] -/
#guard_msgs in
#eval [isEven 4, isEven 5]

使用 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 and evaluating it. * 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 实例。

Displaying Output

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 and evaluating it. * 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

Live ↪

option

eval.pp

Default value: true

('#eval' command) enables using 'ToExpr' instances to pretty print the result, otherwise uses 'Repr' or 'ToString' instances

option

eval.type

Default value: false

('#eval' command) enables pretty printing the type of the result

option

eval.derive.repr

Default value: true

('#eval' command) enables auto-deriving 'Repr' instances as a fallback

通过定义合适的 MonadLiftMonadLift 在有关提升 monad 的部分或 MonadEval 实例中描述，可以赋予 Monad 在 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * 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 的其他实例。

type class

MonadEval.{u, v, w} (m : semiOutParam (Type u → Type v))
  (n : Type u → Type w) : Type (max (max (u + 1) v) w)
MonadEval.{u, v, w}
  (m : semiOutParam (Type u → Type v))
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

Typeclass used for adapting monads. This is similar to MonadLift, but instances are allowed to make use of default state for the purpose of synthesizing such an instance, if necessary. Every MonadLift instance gives a MonadEval instance.

The purpose of this class is for the #eval command, which looks for a MonadEval m CommandElabM or MonadEval m IO instance.

Instance Constructor

MonadEval.mk.{u, v, w}

Methods

monadEval : {α : Type u} → m α → n α

Evaluates a value from monad m into monad n.

type class

MonadEvalT.{u, v, w} (m : Type u → Type v) (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)
MonadEvalT.{u, v, w} (m : Type u → Type v)
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

The transitive closure of MonadEval.

Instance Constructor

MonadEvalT.mk.{u, v, w}

Methods

monadEval : {α : Type u} → m α → n α

Evaluates a value from monad m into monad 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 and evaluating it. * 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 and evaluating it. * 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 更适合计算项的值。特别是，使用良基递归或部分固定点定义的函数要么使用归约引擎计算非常慢，要么根本不会归约。

syntaxReducing Terms

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 Configuration for the `#reduce` command. ((ident := term))* term

#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.

Reducing Functions

减少一项会导致 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

Live ↪

3.3. 检查类型🔗

syntaxChecking Types

#check 可用于详细说明术语并检查其类型。

command ::= ...
    | #check term

如果提供的术语是全局常量名称的标识符，则 #check 打印其签名。否则，该术语将被详细说明为 Lean 术语并打印其类型。

Lean.Parser.Command.check : command#check 中的术语精化不要求对该术语进行充分精化；它可能包含元变量。如果所写的项可能具有类型，则精化成功。如果永远无法合成所需的实例，则精化失败；由元变量引起的综合问题不会阻止精化。

#check and Underdetermined Types

在此示例中，列表元素的类型未确定，因此该类型包含一个元变量：

fun x => [x] : ?m.4 → List ?m.4#check fun x => [x]

fun x => [x] : ?m.4 → List ?m.4

在此示例中，所添加的项的类型和加法的结果类型都是未知的，因为HAdd允许添加不同类型的项。在幕后，元变量代表未知的 HAdd 实例。

fun x => x + x : (x : ?m.7) → ?m.8 x#check fun x => x + x

fun x => x + x : (x : ?m.7) → ?m.8 x

Live ↪

syntaxTesting Type Errors

command ::= ...
    | #check_failure term

Lean.Parser.Command.check : command#check 的此变体使用与 Lean.Parser.Command.check : command#check 相同的过程来详细精化该术语。如果精化成功，则为错误；如果失败，则没有错误。部分精化的术语和发现的任何类型信息都将添加到消息日志。

Checking for Type Errors

正如预期的那样，尝试将字符串添加到自然数失败：

"one" + 1 : ?m.5#check_failure failed to synthesize instance of type class
  HAdd String Nat ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command."one" + 1

failed to synthesize instance of type class
  HAdd String Nat ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

尽管如此，还是有一个部分精化的术语：

"one" + 1 : ?m.5

Live ↪

3.4. 综合实例🔗

syntaxSynthesizing Instances

command ::= ...
    | #synth term

Lean.Parser.Command.synth : command#synth 命令调用 Lean 的类型类解析机制，并尝试执行实例合成来查找给定类型类的实例。如果成功，则输出结果实例项。

Synthesizing a Type Class Instance

Lean 使用类型类来重载加法等操作。 + 运算符是调用 HAdd.hAdd 的符号，它是 HAdd 类型类中的单个方法。此示例显示 Lean 让我们将两个整数相加，结果将是一个整数：

instHAdd#synth HAdd Int Int Int

instHAdd

默认情况下，Lean 不显示输出项中的隐式参数。然而，实例参数是隐式的，这降低了此输出对于理解实例综合的有用性。将选项 pp.explicit 设置为 true 会导致 Lean 显示隐式参数，包括实例：

set_option pp.explicit true in
@instHAdd Int Int.instAdd#synth HAdd Int Int Int

@instHAdd Int Int.instAdd

Lean 不允许添加整数和字符串，如类型类实例合成失败所示：

failed to synthesize
  HAdd Int String String

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.#synth HAdd Int String String

failed to synthesize
  HAdd Int String String

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.5. 查询上下文🔗

#print 系列命令用于查询 Lean 以获取有关定义的信息。

syntaxPrinting Definitions

command ::= ...
    | #print ident

打印常量的定义。

使用 Lean.Parser.Command.print : command#print 打印定义会将定义打印为术语。使用策略证明的定理在打印为项时可能会非常大。

syntaxPrinting Strings

command ::= ...
    | #print str

将字符串文字添加到 Lean 的消息日志。

syntaxPrinting Axioms

command ::= ...
    | Prints the axioms used by a declaration, directly or indirectly.
Please consult [the reference manual](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=validating-proofs) to understand the significance of the output. #print axioms ident

列出常量传递依赖的所有公理。有关更多信息，请参阅公理文档。

Printing Axioms

这两个函数各自交换一对位向量中的元素：

def swap (x y : BitVec 32) : BitVec 32 × BitVec 32 :=
  (y, x)

def swap' (x y : BitVec 32) : BitVec 32 × BitVec 32 :=
  let x := x ^^^ y
  let y := x ^^^ y
  let x := x ^^^ y
  (x, y)

使用函数扩展性、简化器和 bv_decide 可以证明它们是相等的：

theorem swap_eq_swap' : swap = swap' := by⊢ swap = swap'
  funext x yx:BitVec 32y:BitVec 32⊢ swap x y = swap' x y
  simp only [swap, swap', Prod.mk.injEq]x:BitVec 32y:BitVec 32⊢ y = x ^^^ y ^^^ (x ^^^ y ^^^ y) ∧ x = x ^^^ y ^^^ y
  bv_decideAll goals completed! 🐙

由此产生的证明使用了许多公理：

'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Quot.sound, swap_eq_swap'._native.bv_decide.ax_3]#print axioms swap_eq_swap'

'swap_eq_swap'' depends on axioms: [propext, Classical.choice, Quot.sound, swap_eq_swap'._native.bv_decide.ax_3]

公理 swap_eq_swap'._native.bv_decide.ax_3 由 bv_decide 生成，表明本机代码用于将外部证明证书转换为 Lean 证明项。

Live ↪

syntaxPrinting Equations

命令 Lean.Parser.Command.printEqns : command#print equations（可缩写为 Lean.Parser.Command.printEqns : command#print eqns）显示函数的方程引理。

command ::= ...
    | #print equations ident

command ::= ...
    | #print eqns ident

Printing Equations

def intersperse (x : α) : List α → List α
  | y :: z :: zs => y :: x :: intersperse x (z :: zs)
  | xs => xs

equations:
@[backward_defeq] theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
  intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
  (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1#print equations intersperse

equations:
@[backward_defeq] theorem intersperse.eq_1.{u_1} : ∀ {α : Type u_1} (x y z : α) (zs : List α),
  intersperse x (y :: z :: zs) = y :: x :: intersperse x (z :: zs)
theorem intersperse.eq_2.{u_1} : ∀ {α : Type u_1} (x : α) (x_1 : List α),
  (∀ (y z : α) (zs : List α), x_1 = y :: z :: zs → False) → intersperse x x_1 = x_1

它不打印定义方程，也不打印展开方程：

intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) :
  intersperse x x✝ =
    match x✝ with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs#check intersperse.eq_def

intersperse.eq_def.{u_1} {α : Type u_1} (x : α) (x✝ : List α) :
  intersperse x x✝ =
    match x✝ with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs

intersperse.eq_unfold.{u_1} :
  @intersperse = fun {α} x x_1 =>
    match x_1 with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs#check intersperse.eq_unfold

intersperse.eq_unfold.{u_1} :
  @intersperse = fun {α} x x_1 =>
    match x_1 with
    | y :: z :: zs => y :: x :: intersperse x (z :: zs)
    | xs => xs

Live ↪

syntaxScope Information

#where gives a description of the state of the current scope scope. This includes the current namespace, open namespaces, universe and variable commands, and options set with set_option.

command ::= ...
    | `#where` gives a description of the state of the current scope scope.
This includes the current namespace, `open` namespaces, `universe` and `variable` commands,
and options set with `set_option`.
#where

Scope Information

Lean.Parser.Command.where : command`#where` gives a description of the state of the current scope scope. This includes the current namespace, `open` namespaces, `universe` and `variable` commands, and options set with `set_option`.#where 命令显示对当前节范围所做的所有修改，无论是在当前范围还是在其嵌套的范围中。

section
open Nat

namespace A
variable (n : Nat)
namespace B

open List
set_option pp.funBinderTypes true

namespace A.B

open Nat List

variable (n : Nat)

set_option pp.funBinderTypes true
set_option pp.tagAppFns true#where

end A.B
end

namespace A.B

open Nat List

variable (n : Nat)

set_option pp.funBinderTypes true
set_option pp.tagAppFns true

Live ↪

syntaxChecking the Lean Version

Shows the current Lean version. Prints Lean.versionString.

command ::= ...
    | Shows the current Lean version. Prints `Lean.versionString`. #version

3.6. 使用 `#guard_msgs` 测试输出🔗

Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 命令可用于确保命令输出的消息符合预期。与本节中的交互命令一起，它可用于构造一个文件，该文件仅在输出符合预期时才会详细说明；这样的文件可以用作 Lake 中的测试驱动程序。

syntaxDocumenting Expected Output

command ::= ...
    | `/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.

Basic example:
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.

By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```

In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is
`(check all, whitespace := normalized, ordering := exact, positions := false)`.

Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.

The filters can be prefixed with the action to take:
- `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.

Whitespace handling (after trimming leading and trailing whitespace):
- `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.

Message ordering:
- `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.

Position reporting:
- `positions := true` reports the ranges of all messages relative to the line on which
  `#guard_msgs` appears.
- `positions := false` does not report position info.

Substring matching:
- `substring := true` checks that the docstring appears as a substring of the output
  (after whitespace normalization). This is useful when you only care about part of the message.
- `substring := false` (the default) requires exact matching (modulo whitespace normalization).

Stabilizing output:
When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may
differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace
anonymous metavariables with `?_` while preserving user-named metavariables like `?a`.
Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`.
Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like
`_fvar.22` with `_fvar._`.

For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
everything else.

The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
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.
docComment?
      #guard_msgs ((guardMsgsSpecElt,*))? in
      command

/-- ... -/ #guard_msgs in cmd captures the messages generated by the command cmd and checks that they match the contents of the docstring.

Basic example:

/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x

This checks that there is such an error and then consumes the message.

By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings:

/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry

or only errors

#guard_msgs(error) in
declaration uses `sorry`example : α := sorry

In the previous example, since warnings are not captured there is a warning on sorry. We can drop the warning completely with

#guard_msgs(error, drop warning) in
example : α := sorry

In general, #guard_msgs accepts a comma-separated list of configuration clauses in parentheses:

#guard_msgs (

By default, the configuration list is (check all, whitespace := normalized, ordering := exact, positions := false).

Message filters select messages by severity:

info, warning, error: (non-trace) messages with the given severity level.
trace: trace messages
all: all messages.

The filters can be prefixed with the action to take:

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.

Whitespace handling (after trimming leading and trailing whitespace):

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.

Message ordering:

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.

Position reporting:

positions := true reports the ranges of all messages relative to the line on which #guard_msgs appears.
positions := false does not report position info.

Substring matching:

substring := true checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message.
substring := false (the default) requires exact matching (modulo whitespace normalization).

Stabilizing output: When messages contain autogenerated names (e.g., metavariables like ?m.47), the output may differ between runs or Lean versions. Use set_option pp.mvars.anonymous false to replace anonymous metavariables with ?_ while preserving user-named metavariables like ?a. Alternatively, set_option pp.mvars false replaces all metavariables with ?_. Similarly, set_option pp.fvars.anonymous false replaces loose free variable names like _fvar.22 with _fvar._.

For example, #guard_msgs (error, drop all) in cmd means to check errors and drop everything else.

The command elaborator has special support for #guard_msgs for linting. The #guard_msgs itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for all top-level commands, which would include #guard_msgs itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if #guard_msgs is not present.

Testing Return Values

def reverse : List α → List α := helper []
where
  helper acc
    | [] => acc
    | x :: xs => helper (x :: acc) xs

/-- info: [] -/
#guard_msgs in
#eval reverse ([] : List Nat)

/-- info: ['c', 'b', 'a'] -/
#guard_msgs in
#eval reverse "abc".toList

Live ↪

可以通过三种方式指定 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 命令的行为：

提供一个过滤器来选择要检查的消息子集
指定空白比较策略
决定按消息内容或消息生成顺序对消息进行排序

这些配置选项在括号中提供，并用逗号分隔。

syntaxSpecifying #guard_msgs Behavior

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.
guardMsgsFilter

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.
whitespace := guardMsgsWhitespaceArg

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.
ordering := guardMsgsOrderingArg

Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 共有三种选项：过滤器、空白比较策略和排序。

syntaxOutput Filters for #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.
guardMsgsFilter ::=
    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.
drop? all

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.
guardMsgsFilter ::= ...
    | 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.
drop? info

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.
guardMsgsFilter ::= ...
    | 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.
drop? warning

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.
guardMsgsFilter ::= ...
    | 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.
drop? error

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.

syntaxWhitespace Comparison for #guard_msgs

guardMsgsWhitespaceArg ::=
    exact

guardMsgsWhitespaceArg ::= ...
    | lax

guardMsgsWhitespaceArg ::= ...
    | normalized

比较消息时，始终忽略前导和尾随空格。除此之外，还可以使用以下设置：

whitespace := exact 需要精确的空格匹配。
whitespace := normalized 在匹配之前将所有换行符转换为空格（默认）。这允许打破长线。
whitespace := lax 在匹配之前将空格折叠为单个空格。

选项 guard_msgs.diff 控制当预期消息与生成的消息不匹配时 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 生成的错误消息的内容。默认情况下，Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 显示逐行差异，前导 + 用于指示生成消息中的行，前导 - 用于指示预期消息中的行。当消息很大且差异很小时，这可以更容易地注意到它们的差异。将 guard_msgs.diff 设置为 false 会导致 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#guard_msgs 仅显示生成的消息，该消息可以与源文件中的预期消息进行比较。如果消息之间的差异令人困惑或难以承受，这会很方便。

option

guard_msgs.diff

Default value: true

When true, show a diff between expected and actual messages if they don't match.

Displaying Differences

Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#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
/--
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]]]
-/
❌️ 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` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `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. Whitespace handling (after trimming leading and trailing whitespace): - `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. Message ordering: - `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. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present.#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
/--
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]]]
-/
❌️ 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]]]

Live ↪

3.7. 技术输出🔗

Repr 类型类用于提供可解析和评估以获得等效值的数据的标准表示形式。这不是一个严格的正确性标准：对于某些类型，尤其是那些带有嵌入命题的类型，这是不可能实现的。但是，Repr 实例生成的输出应尽可能接近可解析和评估的输出。

除了机器可读之外，这种表示形式还应该方便人们理解，特别是行不应该太长，嵌套值应该缩进。这是通过两步过程实现的：

Repr 实例生成 Std.Format 类型的中间文档，它紧凑地表示一组在换行符和缩进位置方面有所不同的字符串。
渲染过程根据所需的最大线长度等标准从集合中选择“最佳”代表。

特别是，Std.Format 可以组合构建，因此 Repr 实例不需要考虑周围的缩进上下文。

3.7.1. 格式🔗

Format此处描述的 API 是 Wadler 的 (Philip Wadler, 2003. “A Prettier Printer”. In The Fun of Programming, A symposium in honour of Professor Richard Bird's 60th birthday.) 的改编版，它已被修改为在严格的语言中高效，并支持元数据标签等附加功能。是一组字符串的紧凑表示。最重要的 Format 操作是：

弦乐: 可以使用 text 构造函数将 String 制作为 Format。此构造函数注册为从 String 到 Format 的强制，因此通常不需要显式调用它。 text str 表示仅包含 str 的单例集。如果字符串包含换行符 ('\n')，则它们将无条件作为换行符插入到结果输出中，无论组如何。但是，它们会根据当前的缩进级别进行缩进。
追加: 可以使用 Append Format 实例中的 ++ 运算符附加两个 Format。
组和换行符: 构造函数 line 表示同时包含 "\n" ++ indent 和 " " 的集合，其中 indent 是一个具有足够空格以正确缩进该行的字符串。无论如何，它可以被认为是一个换行符，如果当前行有足够的空间，它将被“展平”到一个空格。换行符出现在groups中：group 运算符的最近封闭应用程序确定换行符属于哪个组。默认情况下，组中的所有 line 代表 "\n"，或者全部代表 " "；组也可以配置为填充行，在这种情况下，组中最小数量的 line 代表 "\n"。不属于组的 line 的使用始终代表 "\n"。
缩进: 插入换行符时，输出也会缩进。 nest n 将文档的缩进增加 n 空格。这不足以表示所有 Lean 语法，有时需要列精确对齐。 align 是一个文档，可确保输出字符串处于当前缩进级别，如果可能的话仅插入空格，或者如果需要则插入换行符后跟空格。
标记: Lean 的交互功能需要能够将输出与其所表示的基础值关联起来。例如，这允许 Lean 开发环境在将鼠标悬停在术语证明状态或错误消息上时呈现详细的术语。可以使用 tag n 使用 Nat 值 n 对文档进行“标记”；这些 Nat 应映射到侧表中的基础值。

Widths and Newlines

open Std Format

帮助器 parenSeq 创建一个带括号的序列，具有分组和缩进，以使其响应不同的输出宽度。

def parenSeq (xs : List Format) : Format :=
  group <|
    nest 2 (text "(" ++ line ++ joinSep xs line) ++
    line ++
    ")"

该文档表示带括号的数字序列：

def lst : Format := parenSeq nums
where nums := [1, 2, 3, 4, 5].map (text s!"{·}")

使用 120 个字符的默认行宽进行渲染会将整个序列放在一行上：

( 1 2 3 4 5 )
#eval IO.println lst.pretty

( 1 2 3 4 5 )

由于所有 line 都属于同一个 group，因此它们要么全部呈现为空格，要么全部呈现为换行符。如果只有 9 个字符可用，则 lst 中的所有 line 都将成为换行符：

(
  1
  2
  3
  4
  5
)
#eval IO.println (lst.pretty (width := 9))

本文档包含 lst 的三个副本，按进一步的括号顺序排列：

def lsts := parenSeq [lst, lst, lst]

在默认宽度下，它保持在一行上：

( ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) )
#eval IO.println lsts.pretty

( ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) ( 1 2 3 4 5 ) )

如果只有 20 个可用字符，则每次出现 lst 时都会独占一行。这是因为将外部 group 转换为换行符足以将字符串保持在 20 列之内：

(
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
)
#eval IO.println (lsts.pretty (width := 20))

(
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
  ( 1 2 3 4 5 )
)

如果只有 10 个字符，则每个数字必须独占一行：

(
  (
    1
    2
    3
    4
    5
  )
  (
    1
    2
    3
    4
    5
  )
  (
    1
    2
    3
    4
    5
  )
)
#eval IO.println (lsts.pretty (width := 10))

Live ↪

Grouping and Filling

open Std Format

帮助器 parenSeq 创建一个带括号的序列，每个元素放置在一个新行并缩进：

def parenSeq (xs : List Format) : Format :=
  nest 2 (text "(" ++ line ++ joinSep xs line) ++
  line ++
  ")"

nums 包含数字 1 到 20，作为格式列表：

def nums : List Format :=
  Nat.fold 20 (init := []) fun i _ ys =>
    text s!"{20 - i}" :: ys

[Std.Format.text "1",
 Std.Format.text "2",
 Std.Format.text "3",
 Std.Format.text "4",
 Std.Format.text "5",
 Std.Format.text "6",
 Std.Format.text "7",
 Std.Format.text "8",
 Std.Format.text "9",
 Std.Format.text "10",
 Std.Format.text "11",
 Std.Format.text "12",
 Std.Format.text "13",
 Std.Format.text "14",
 Std.Format.text "15",
 Std.Format.text "16",
 Std.Format.text "17",
 Std.Format.text "18",
 Std.Format.text "19",
 Std.Format.text "20"]#eval nums

由于 parenSeq 不引入任何组，因此生成的文档将呈现在一行上：

(
  1
  2
  3
  4
  5
  6
  7
  8
  9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
)
#eval IO.println (pretty (parenSeq nums))

这可以通过对它们进行分组来解决。 grouped 使用 group 执行此操作，而 filled 使用 fill 执行此操作。

def grouped := group (parenSeq nums)
def filled := fill (parenSeq nums)

两个分组运算符都会导致使用 line 呈现为空格。如果有足够的空间，两者都会呈现在一行上：

( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )
#eval IO.println (pretty grouped)

( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )

( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )
#eval IO.println (pretty filled)

( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )

然而，当单行上没有足够的空间时，差异就会变得明显。除非 group 中的所有换行符都可以是空格，否则都不能：

(
  1
  2
  3
  4
  5
  6
  7
  8
  9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
)
#eval IO.println (pretty (width := 30) grouped)

另一方面，使用 fill 仅根据需要插入换行符以避免出现两宽：

( 1 2 3 4 5 6 7 8 9 10 11 12
  13 14 15 16 17 18 19 20 )
#eval IO.println (pretty (width := 30) filled)

( 1 2 3 4 5 6 7 8 9 10 11 12
  13 14 15 16 17 18 19 20 )

使用较长的序列可以清楚地看到 fill 的行为：

( 1 2 3 4 5 6 7 8 9 10 11 12
  13 14 15 16 17 18 19 20 1 2
  3 4 5 6 7 8 9 10 11 12 13 14
  15 16 17 18 19 20 1 2 3 4 5
  6 7 8 9 10 11 12 13 14 15 16
  17 18 19 20 1 2 3 4 5 6 7 8
  9 10 11 12 13 14 15 16 17 18
  19 20 )
#eval IO.println <|
  pretty (width := 30) (fill (parenSeq (nums ++ nums ++ nums ++ nums)))

( 1 2 3 4 5 6 7 8 9 10 11 12
  13 14 15 16 17 18 19 20 1 2
  3 4 5 6 7 8 9 10 11 12 13 14
  15 16 17 18 19 20 1 2 3 4 5
  6 7 8 9 10 11 12 13 14 15 16
  17 18 19 20 1 2 3 4 5 6 7 8
  9 10 11 12 13 14 15 16 17 18
  19 20 )

Live ↪

Newline Characters in Strings

在字符串中包含换行符会导致渲染过程无条件插入换行符。然而，这些换行符确实尊重当前的缩进级别。

文档 str 由带有两个换行符的嵌入字符串组成：

open Std Format

def str : Format := text "abc\nxyz\n123"

打印带分组和不带分组的字符串都会导致使用换行符：

abc
xyz
123
#eval IO.println str.pretty

abc
xyz
123

abc
xyz
123
#eval IO.println (group str).pretty

abc
xyz
123

由于字符串不以换行符结尾，因此第一个字符串的最后一行与第二个字符串的第一行位于同一行：

abc
xyz
123abc
xyz
123
#eval IO.println (str ++ str).pretty

abc
xyz
123abc
xyz
123

但是，增加缩进级别会导致字符串的所有三行都从同一列开始：

It is:
  abc
  xyz
  123
#eval IO.println (text "It is:" ++ indentD str).pretty

It is:
  abc
  xyz
  123

It is:  abc
        xyz
        123
#eval IO.println (nest 8 <| text "It is:" ++ align true ++ str).pretty

It is:  abc
        xyz
        123

Live ↪

3.7.1.1. 文件🔗

inductive type

Std.Format : Type
Std.Format : Type

A representation of a set of strings, in which the placement of newlines and indentation differ.

Given a specific line width, specified in columns, the string that uses the fewest lines can be selected.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

Constructors

Std.Format.nil : Std.Format

The empty format.

Std.Format.line : Std.Format

A position where a newline may be inserted if the current group does not fit within the allotted column width.

Std.Format.align (force : Bool) : Std.Format

align tells the formatter to pad with spaces to the current indentation level, or else add a newline if we are already at or past the indent.

If force is true, then it will pad to the indent even if it is in a flattened group.

Example:

open Std Format in
#eval IO.println (nest 2 <| "." ++ align ++ "a" ++ line ++ "b")

. a
  b

Std.Format.text : String → Std.Format

A node containing a plain string.

If the string contains newlines, the formatter emits them and then indents to the current level.

Std.Format.nest (indent : Int) (f : Std.Format) : Std.Format

nest indent f increases the current indentation level by indent while rendering f.

Example:

open Std Format in
def fmtList (l : List Format) : Format :=
  let f := joinSep l  (", " ++ Format.line)
  group (nest 1 <| "[" ++ f ++ "]")

This will be written all on one line, but if the text is too large, the formatter will put in linebreaks after the commas and indent later lines by 1.

Std.Format.append : Std.Format → Std.Format → Std.Format

Concatenation of two Formats.

Std.Format.group :
  Std.Format →
    (behavior :
        optParam Std.Format.FlattenBehavior
          Std.Format.FlattenBehavior.allOrNone) →
      Std.Format

Creates a new flattening group for the given inner Format.

Std.Format.tag : Nat → Std.Format → Std.Format

Used for associating auxiliary information (e.g. Exprs) with Format objects.

inductive type

Std.Format.FlattenBehavior : Type
Std.Format.FlattenBehavior : Type

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

allOrNone will make a linebreak on every Format.line in the group or none of them.
[1, 2, 3]
fill will only make linebreaks on as few Format.lines as possible:
[1, 2, 3]

Constructors

Std.Format.FlattenBehavior.allOrNone :
  Std.Format.FlattenBehavior

Either all Format.lines in the group will be newlines, or all of them will be spaces.

Std.Format.FlattenBehavior.fill : Std.Format.FlattenBehavior

As few Format.lines in the group as possible will be newlines.

def

Std.Format.fill (f : Std.Format) : Std.Format
Std.Format.fill (f : Std.Format) :
  Std.Format

Creates a group in which as few Format.lines as possible are rendered as newlines.

This is an alias for Format.group, with FlattenBehavior set to fill.

3.7.1.2. 空文档🔗

空字符串在 Std.Format 中没有唯一的代表。以下所有内容都代表空字符串：

.nil
.text ""
.text "" ++ .nil
.nil ++ .text ""

使用 Std.Format.isEmpty 检查文档是否包含零个字符，使用 Std.Format.isNil 专门检查它是否是构造函数 Std.Format.nil。

def

Std.Format.isEmpty : Std.Format → Bool
Std.Format.isEmpty : Std.Format → Bool

Checks whether the given format contains no characters.

def

Std.Format.isNil : Std.Format → Bool
Std.Format.isNil : Std.Format → Bool

Checks whether a Format is the constructor Format.nil.

This does not check whether the resulting rendered strings are always empty. To do that, use Format.isEmpty.

3.7.1.3. 序列🔗

当存在某种重复内容（例如列表的元素）时，本节中的运算符非常有用。这通常是通过使用包围运算符在其分隔符参数中包含 line 来完成的

def

Std.Format.join (xs : List Std.Format) : Std.Format
Std.Format.join (xs : List Std.Format) :
  Std.Format

Concatenates a list of Formats with ++.

def

Std.Format.joinSep.{u} {α : Type u} [Std.ToFormat α] :
  List α → Std.Format → Std.Format
Std.Format.joinSep.{u} {α : Type u}
  [Std.ToFormat α] :
  List α → Std.Format → Std.Format

Intercalates the given list with the given sep format.

The list items are formatting using ToFormat.format.

def

Std.Format.prefixJoin.{u} {α : Type u} [Std.ToFormat α]
  (pre : Std.Format) : List α → Std.Format
Std.Format.prefixJoin.{u} {α : Type u}
  [Std.ToFormat α] (pre : Std.Format) :
  List α → Std.Format

Concatenates the given list after prepending pre to each element.

The list items are formatting using ToFormat.format.

def

Std.Format.joinSuffix.{u} {α : Type u} [Std.ToFormat α] :
  List α → Std.Format → Std.Format
Std.Format.joinSuffix.{u} {α : Type u}
  [Std.ToFormat α] :
  List α → Std.Format → Std.Format

Concatenates the given list after appending the given suffix to each element.

The list items are formatting using ToFormat.format.

3.7.1.4. 缩进🔗

这些运算符可以更轻松地在 Std.Format.nest 之上实现一致的缩进样式。

def

Std.Format.nestD (f : Std.Format) : Std.Format
Std.Format.nestD (f : Std.Format) :
  Std.Format

Increases the indentation level by the default amount.

def

Std.Format.defIndent : Nat
Std.Format.defIndent : Nat

The default indentation level, which is two spaces.

def

Std.Format.indentD (f : Std.Format) : Std.Format
Std.Format.indentD (f : Std.Format) :
  Std.Format

Insert a newline and then f, all nested by the default indent amount.

3.7.1.5. 方括号和圆括号🔗

这些运算符可以更轻松地实现一致的括号样式。

def

Std.Format.bracket (l : String) (f : Std.Format) (r : String) :
  Std.Format
Std.Format.bracket (l : String)
  (f : Std.Format) (r : String) :
  Std.Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is allOrNone; for fill use Std.Format.bracketFill.

def

Std.Format.sbracket (f : Std.Format) : Std.Format
Std.Format.sbracket (f : Std.Format) :
  Std.Format

Creates the format "[" ++ f ++ "]" with a flattening group, nesting by one space.

sbracket is short for “square bracket”.

def

Std.Format.paren (f : Std.Format) : Std.Format
Std.Format.paren (f : Std.Format) :
  Std.Format

Creates the format "(" ++ f ++ ")" with a flattening group, nesting by one space.

def

Std.Format.bracketFill (l : String) (f : Std.Format) (r : String) :
  Std.Format
Std.Format.bracketFill (l : String)
  (f : Std.Format) (r : String) :
  Std.Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is fill; for allOrNone use Std.Format.bracketFill.

3.7.1.6. 渲染🔗

ToString Std.Format 实例使用其默认参数调用 Std.Format.pretty。

有两种方式呈现文档：

使用 pretty 构造 String。必须先构建整个字符串，然后才能将任何字符串发送给用户。
使用 prettyM 增量发射 String，并使用某些 Monad 中的效果。一旦每行被渲染，它就会被发射。这适合流式输出。

def

Std.Format.pretty (f : Std.Format) (width : Nat := Std.Format.defWidth)
  (indent column : Nat := 0) : String
Std.Format.pretty (f : Std.Format)
  (width : Nat := Std.Format.defWidth)
  (indent column : Nat := 0) : String

Renders a Format to a string.

width: the total width
indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)
column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)

def

Std.Format.defWidth : Nat
Std.Format.defWidth : Nat

The default width of the targeted output, which is 120 columns.

def

Std.Format.prettyM {m : Type → Type} (f : Std.Format) (w : Nat)
  (indent : Nat := 0) [Monad m] [Std.Format.MonadPrettyFormat m] :
  m Unit
Std.Format.prettyM {m : Type → Type}
  (f : Std.Format) (w : Nat)
  (indent : Nat := 0) [Monad m]
  [Std.Format.MonadPrettyFormat m] :
  m Unit

Renders a Format using effects in the monad m, using the methods of MonadPrettyFormat.

Each line is emitted as soon as it is rendered, rather than waiting for the entire document to be rendered.

w: the total width
indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)

type class

Std.Format.MonadPrettyFormat (m : Type → Type) : Type
Std.Format.MonadPrettyFormat
  (m : Type → Type) : Type

A monad that can be used to incrementally render Format objects.

Instance Constructor

Std.Format.MonadPrettyFormat.mk

Methods

pushOutput : String → m Unit

Emits the string s.

pushNewline : Nat → m Unit

Emits a newline followed by indent columns of indentation.

currColumn : m Nat

Gets the current column at which the next string will be emitted.

startTag : Nat → m Unit

Starts a region tagged with tag.

endTags : Nat → m Unit

Exits the scope of count opened tags.

3.7.1.7. `ToFormat` 级🔗

Std.ToFormat 类用于提供格式化值的标准方法，但不期望此格式化是有效的 Lean 语法。这些实例用于错误消息和某些序列连接运算符。

type class

Std.ToFormat.{u} (α : Type u) : Type u
Std.ToFormat.{u} (α : Type u) : Type u

Specifies a “user-facing” way to convert from the type α to a Format object. There is no expectation that the resulting string is valid code.

The Repr class is similar, but the expectation is that instances produce valid Lean code.

Instance Constructor

Std.ToFormat.mk.{u}

Methods

format : α → Std.Format

Converts a value to a Format object, with no expectation that the resulting string is valid code.

3.7.2. `Repr`🔗

Repr 实例描述如何将值表示为 Std.Format。因为它们应该发出有效的 Lean 语法，所以这些实例需要考虑优先级。插入最大数量的括号是可行的，但它使人们更难以阅读结果输出。

type class

Repr.{u} (α : Type u) : Type u
Repr.{u} (α : Type u) : Type u

The standard way of turning values of some type into Format.

When rendered this Format should be as close as possible to something that can be parsed as the input value.

Instance Constructor

Repr.mk.{u}

Methods

reprPrec : α → Nat → Std.Format

Turn a value of type α into a Format at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.

def

repr.{u_1} {α : Type u_1} [Repr α] (a : α) : Std.Format
repr.{u_1} {α : Type u_1} [Repr α]
  (a : α) : Std.Format

Turns a into a Format using its Repr instance. The precedence level is initially set to 0.

def

reprStr.{u_1} {α : Type u_1} [Repr α] (a : α) : String
reprStr.{u_1} {α : Type u_1} [Repr α]
  (a : α) : String

Turns a into a String using its Repr instance, rendering the Format at the default width of 120 columns.

The precedence level is initially set to 0.

Maximal Parentheses

NatOrInt 类型可以包含 Nat 或 Int：

inductive NatOrInt where
  | nat : Nat → NatOrInt
  | int : Int → NatOrInt

此 Repr NatOrInt 实例通过插入许多括号来确保输出是有效的 Lean 语法：

instance : Repr NatOrInt where
  reprPrec x _ :=
    .nestD <| .group <|
      match x with
      | .nat n =>
          .text "(" ++ "NatOrInt.nat" ++ .line ++ "(" ++ repr n ++ "))"
      | .int i =>
          .text "(" ++ "NatOrInt.int" ++ .line ++ "(" ++ repr i ++ "))"

无论它包含 Nat、非负 Int 还是负 Int，都可以解析结果：

open NatOrInt in
(NatOrInt.nat (3))
(NatOrInt.int (5))
(NatOrInt.int (-5))
#eval do
  IO.println <| repr <| nat 3
  IO.println <| repr <| int 5
  IO.println <| repr <| int (-5)

(NatOrInt.nat (3))
(NatOrInt.int (5))
(NatOrInt.int (-5))

但是，(NatOrInt.nat (3)) 并不是特别惯用的 Lean，并且多余的括号可能会导致读取大型表达式变得困难。

Live ↪

方法 Repr.reprPrec 具有以下签名：

Repr.reprPrec.{u} {α : Type u} [Repr α] : α → Nat → Std.Format

第一个显式参数是要表示的值，而第二个参数是它出现的上下文的 precedence。此优先级可用于决定是否插入括号：如果实例生成的语法的优先级大于其上下文的优先级，则需要括号。

3.7.2.1. 如何编写 `Repr` 实例🔗

Lean 可以使用实例派生自动为大多数类型生成适当的 Repr 实例。然而，在某些情况下，有必要手动编写一个实例：

编写自定义 Repr 实例时，请遵循以下约定：

优先级

检查优先级，根据需要添加括号，并将正确的优先级传递给嵌入数据的 reprPrec 实例。如果需要，每个实例都有责任将自己括在括号中；实例通常不应将对 reprPrec 的递归调用括起来。

函数应用程序具有最高优先级，max_prec。帮助程序 Repr.addAppParen 和 reprArg 分别在需要时在应用程序周围插入括号，并将适当的优先级传递给函数参数。

完全限定名称

Repr 实例确实有权访问给定位置的开放命名空间集。环境中常量的所有名称都应该完全限定以消除歧义。

默认嵌套

嵌套数据应使用 nestD 缩进，以确保跨实例的缩进一致。

分组和换行

每个包含换行符的 Repr 实例的输出应包含在 group 中。此外，如果生成的代码包含嵌套的概念表达式，则应在每个嵌套级别周围插入 group。通常应在以下位置插入换行符：

在构造函数及其每个参数之间
:=之后
,之后
在结构实例表示法及其内容的左大括号和右大括号之间
在中缀运算符之后，但不是之前

圆括号和方括号

应使用 Std.Format.bracket 或其特化 Std.Format.paren（表示括号）和 Std.Format.sbracket（表示方括号）插入圆括号和方括号。这些运算符以与 Lean 相同的方式对齐括号或方括号表达式的内容。尾随圆括号和方括号不应单独占一行，而应与其内容保持一致。

def

Repr.addAppParen (f : Std.Format) (prec : Nat) : Std.Format
Repr.addAppParen (f : Std.Format)
  (prec : Nat) : Std.Format

Adds parentheses to f if the precedence prec from the context is at least that of function application.

Together with reprArg, this can be used to correctly parenthesize function application syntax.

def

reprArg.{u_1} {α : Type u_1} [Repr α] (a : α) : Std.Format
reprArg.{u_1} {α : Type u_1} [Repr α]
  (a : α) : Std.Format

Turns a into a Format using its Repr instance, with the precedence level set to that of function application.

Together with Repr.addAppParen, this can be used to correctly parenthesize function application syntax.

Inductive Types with Constructors

归纳类型N.NatOrInt 可以包含 Nat 或 Int：

namespace N

inductive NatOrInt where
  | nat : Nat → NatOrInt
  | int : Int → NatOrInt

Repr NatOrInt 实例遵循以下约定：

右侧是函数应用程序，因此它使用 Repr.addAppParen 在必要时添加括号。
括号包裹着整个主体，没有额外的 line。
整个函数应用是分组的，并且嵌套了默认的数量。
通过使用 line 将函数与其参数分开；该换行符通常是一个空格，因为 Repr Nat 和 Repr Int 实例不太可能产生长输出。
对 reprPrec 的递归调用会传递 max_prec，因为它们位于函数参数位置，并且函数应用程序具有最高优先级。

instance : Repr NatOrInt where
  reprPrec
    | .nat n =>
      Repr.addAppParen <|
        .group <| .nestD <|
          "N.NatOrInt.nat" ++ .line ++ reprPrec n max_prec
    | .int i =>
      Repr.addAppParen <|
        .group <| .nestD <|
          "N.NatOrInt.int" ++ .line ++ reprPrec i max_prec

N.NatOrInt.nat 5
#eval IO.println (repr (NatOrInt.nat 5))

N.NatOrInt.nat 5

N.NatOrInt.int 5
#eval IO.println (repr (NatOrInt.int 5))

N.NatOrInt.int 5

N.NatOrInt.int (-5)
#eval IO.println (repr (NatOrInt.int (-5)))

N.NatOrInt.int (-5)

some (N.NatOrInt.int (-5))
#eval IO.println (repr (some (NatOrInt.int (-5))))

some (N.NatOrInt.int (-5))

[N.NatOrInt.nat 0,
 N.NatOrInt.nat 1,
 N.NatOrInt.nat 2,
 N.NatOrInt.nat 3,
 N.NatOrInt.nat 4,
 N.NatOrInt.nat 5,
 N.NatOrInt.nat 6,
 N.NatOrInt.nat 7,
 N.NatOrInt.nat 8,
 N.NatOrInt.nat 9]
#eval IO.println (repr <| (List.range 10).map (NatOrInt.nat))

[N.NatOrInt.nat 0,
 N.NatOrInt.nat 1,
 N.NatOrInt.nat 2,
 N.NatOrInt.nat 3,
 N.NatOrInt.nat 4,
 N.NatOrInt.nat 5,
 N.NatOrInt.nat 6,
 N.NatOrInt.nat 7,
 N.NatOrInt.nat 8,
 N.NatOrInt.nat 9]

[N.NatOrInt.nat
   0,
 N.NatOrInt.nat
   1,
 N.NatOrInt.nat
   2,
 N.NatOrInt.nat
   3,
 N.NatOrInt.nat
   4,
 N.NatOrInt.nat
   5,
 N.NatOrInt.nat
   6,
 N.NatOrInt.nat
   7,
 N.NatOrInt.nat
   8,
 N.NatOrInt.nat
   9]
#eval IO.println <|
  Std.Format.pretty (width := 3) <|
    repr <| (List.range 10).map NatOrInt.nat

[N.NatOrInt.nat
   0,
 N.NatOrInt.nat
   1,
 N.NatOrInt.nat
   2,
 N.NatOrInt.nat
   3,
 N.NatOrInt.nat
   4,
 N.NatOrInt.nat
   5,
 N.NatOrInt.nat
   6,
 N.NatOrInt.nat
   7,
 N.NatOrInt.nat
   8,
 N.NatOrInt.nat
   9]

Live ↪

Infix Syntax

此示例演示了如何使用优先级对左关联漂亮打印机进行编码。 AddExpr 类型表示具有常量和加法的表达式：

inductive AddExpr where
  | nat : Nat → AddExpr
  | add : AddExpr → AddExpr → AddExpr

OfNat 和 Add 实例为 AddExpr 提供更方便的语法：

instance : OfNat AddExpr n where
  ofNat := .nat n

instance : Add AddExpr where
  add := .add

Repr AddExpr 实例应仅插入必要的括号。 Lean 的加法运算符是左关联的，优先级为 65，因此对左侧的递归调用使用优先级 64，并且如果当前上下文的优先级大于或等于 65，则运算符本身会被括号括起来：

protected def AddExpr.reprPrec : AddExpr → Nat → Std.Format
  | .nat n, p  =>
    Repr.reprPrec n p
  | .add e1 e2, p =>
    let out : Std.Format :=
      .nestD <| .group <|
        AddExpr.reprPrec e1 64 ++ " " ++ "+" ++ .line ++
        AddExpr.reprPrec e2 65
    if p ≥ 65 then out.paren else out

instance : Repr AddExpr := ⟨AddExpr.reprPrec⟩

无论输入的括号如何，此实例仅插入必要的括号：

2 + 3 + 4
#eval IO.println (repr (((2 + 3) + 4) : AddExpr))

2 + 3 + 4

2 + 3 + 4
#eval IO.println (repr ((2 + 3 + 4) : AddExpr))

2 + 3 + 4

2 + (3 + 4)
#eval IO.println (repr ((2 + (3 + 4)) : AddExpr))

2 + (3 + 4)

[2 + (3 + 4), 2 + 3 + 4]
#eval IO.println (repr ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr))

[2 + (3 + 4), 2 + 3 + 4]

在实现中使用 group、nestD 和 line 会导致在狭窄的上下文中出现预期的换行符和缩进：

[2 +
   (3 +
      4),
 2 +
     3 +
   4]
#eval ([2 + (3 + 4), (2 + 3) + 4] : List AddExpr)
  |> repr
  |>.pretty (width := 0)
  |> IO.println

[2 +
   (3 +
      4),
 2 +
     3 +
   4]

Live ↪

3.7.2.2. 原子类型🔗

当列表的元素足够小时，用每行一个元素呈现列表可能既难以阅读又浪费空间。为了提高可读性，List 有两个 Repr 实例：一个使用 Std.Format.bracket 作为其内容，另一个使用 Std.Format.bracketFill。后者是在前者之后定义的，因此在可能的情况下选择后者；但是，它需要空类型类 ReprAtom 的实例。

如果某个类型的 Repr 实例从不生成空格或换行符，则它应该有一个 ReprAtom 实例。 Lean 具有 String、UInt8、Nat、Char 和 Bool 等类型的 ReprAtom 实例。

type class

ReprAtom.{u} (α : Type u) : Type
ReprAtom.{u} (α : Type u) : Type

Auxiliary class for marking types that should be considered atomic by Repr methods. We use it at Repr (List α) to decide whether bracketFill should be used or not.

Instance Constructor

ReprAtom.mk.{u}

Atomic Types and Repr

归纳类型ABC 的所有构造函数都不带参数：

inductive ABC where
  | a
  | b
  | c
deriving Repr

派生的 Repr ABC 实例用于显示列表：

def abc : List ABC := [.a, .b, .c]

def abcs : List ABC := abc ++ abc ++ abc

[ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c]
#eval IO.println ((repr abcs).pretty (width := 14))

由于宽度较窄，因此插入换行符：

[ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c,
 ABC.a,
 ABC.b,
 ABC.c]

但是，将列表转换为 List Nat 会导致格式不同的结果。

def ABC.toNat : ABC → Nat
  | .a => 0
  | .b => 1
  | .c => 2

[0, 1, 2, 0,
 1, 2, 0, 1,
 2]#eval IO.print ((repr (abcs.map ABC.toNat)).pretty (width := 14))

换行次数要少得多：

[0, 1, 2, 0,
 1, 2, 0, 1,
 2]

这是因为 ReprAtom Nat 实例的存在。为 ABC 添加一个会导致类似的行为：

instance : ReprAtom ABC := ⟨⟩

[ABC.a, ABC.b,
 ABC.c, ABC.a,
 ABC.b, ABC.c,
 ABC.a, ABC.b,
 ABC.c]
#eval IO.println ((repr abcs).pretty (width := 14))

[ABC.a, ABC.b,
 ABC.c, ABC.a,
 ABC.b, ABC.c,
 ABC.a, ABC.b,
 ABC.c]

Live ↪

3. 与 Lean 交互🔗

3.1. 评估条款🔗

Instance Constructor

Methods

Instance Constructor

Methods

3.2. 减少条款🔗

3.3. 检查类型🔗

3.4. 综合实例🔗

3.5. 查询上下文🔗

3.6. 使用 #guard_msgs 测试输出🔗

3.7. 技术输出🔗

3.7.1. 格式🔗

3.7.1.1. 文件🔗

Constructors

Constructors

3.7.1.2. 空文档🔗

3.7.1.3. 序列🔗

3.7.1.4. 缩进🔗

3.7.1.5. 方括号和圆括号🔗

3.7.1.6. 渲染🔗

Instance Constructor

Methods

3.7.1.7. ToFormat 级🔗

Instance Constructor

Methods

3.7.2. Repr🔗

Instance Constructor

Methods

3.7.2.1. 如何编写 Repr 实例🔗

3.7.2.2. 原子类型🔗

Instance Constructor

3.6. 使用 `#guard_msgs` 测试输出🔗

3.7.1.7. `ToFormat` 级🔗

3.7.2. `Repr`🔗

3.7.2.1. 如何编写 `Repr` 实例🔗