用单书名号括起一个项，表示引用作用域内具有该类型的某个项。
term ::= ...
| 这样便可按定理陈述而非名称引用局部引理，也可引用假设而不论其是否有显式名称。
14.2. 阅读证明状态
证明状态中的目标按顺序显示，主目标位于最上方。
目标可以具名，也可以匿名。
具名目标的顶部以 case 标示（称为分支标签），匿名目标则没有这种标示。
策略会为目标分配名称，通常依据构造器名称、参数名称、结构字段名称，或策略所实现推理步骤的性质来命名。
具名目标
此证明状态包含四个目标，并且全都有名称。
这是证明 Monad Option 实例满足定律（即提供 LawfulMonad Option 实例）的一部分；分支名称（在下方突出显示）来自 LawfulMonad 的字段名。
α:Type ?u.9β:Type ?u.9f:α → βx:Option α⊢ (do
let a ← x
pure (f a)) =
f <$> xα:Type ?u.9β:Type ?u.9f:Option (α → β)x:Option α⊢ (do
let x_1 ← f
x_1 <$> x) =
f <*> xα:Type ?u.9β:Type ?u.9x:αf:α → Option β⊢ pure x >>= f = f xα:Type ?u.9β:Type ?u.9γ:Type ?u.9x:Option αf:α → Option βg:β → Option γ⊢ x >>= f >>= g = x >>= fun x => f x >>= g
可以使用 case 和 case' 策略，按目标名称选择新的主目标。
在本身具名的目标上下文中分配名称时，新目标的名称会附加到主目标名称之后，并以点号（'.', Unicode FULL STOP (0x2e)）分隔。
分层目标名称
每个目标都由一列假设和一个待证结论组成。 每个假设都有名称和类型；结论则是一个类型。 假设要么是某个类型的任意元素，要么是被假定为真的陈述。
假设名称与结论
有些假设是不可访问的， 这意味着无法按名称显式引用它们。
创建假设时未指定名称，或假设名称被后来的假设遮蔽时，就会出现不可访问的假设。
不可访问的假设应视为匿名假设；之所以仍显示得像是具名，是因为后续假设或结论可能引用它们，而显示名称可以区分这些引用。
具体而言，不可访问假设的名称后会显示剑标（†）。
可访问的假设名称
不可访问的假设名称
不可访问的假设仍然可以使用。
assumption 或 simp 等策略可以扫描整个假设列表并找出有用的假设；contradiction 则能找出不可能成立的假设来消除当前目标，而无需为其命名。
rename_i 和 next 等其他策略可以为不可访问的假设命名，使其变得可访问。
此外，还可以把类型写在单书名号中，按类型引用假设。
语法按类型引用假设
按类型引用假设
在以下证明中，反复使用 cases 分析一个数。
证明开始时，这个数名为 x，但 cases 会为后续的数生成不可访问的名称。
该证明没有提供名称，而是利用任一时刻都只有一个 Nat 类型假设这一事实，以 ‹Nat› 引用它。
迭代结束后会有假设 n + 3 < 3，contradiction 可以利用它消除该目标。
example : x < 3 → x ∈ [0, 1, 2] := x:Nat⊢ x < 3 → x ∈ [0, 1, 2]
x:Nata✝:x < 3⊢ x ∈ [0, 1, 2]
iterate 3
a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2]n✝:Nata✝:n✝ + 1 + 1 + 1 < 3⊢ n✝ + 1 + 1 + 1 ∈ [0, 1, 2]
a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2] All goals completed! 🐙
All goals completed! 🐙
证明之外按类型引用假设
14.2.1. 隐藏证明与大型项
证明状态中的项可能相当庞大，假设也可能很多。
由于定义式证明无关性，证明项通常提供不了多少有用信息。
默认情况下，它们不会显示在证明状态的目标中，除非它们是原子的，即不包含子项。
隐藏证明由两个选项控制：pp.proofs 用于开关该功能，pp.proofs.threshold 则确定隐藏证明的大小阈值。
此外，非证明项过大时也可能被隐藏。
具体而言，Lean 会隐藏深度超过可配置阈值的项；总输出量达到一定程度后，也会隐藏项的其余部分。
可以用选项 pp.deepTerms 启用或禁用深层项显示，并用 pp.deepTerms.threshold 配置深度阈值。
美化打印器的最大步数可用选项 pp.maxSteps 配置。
打印非常大的项可能导致工具变慢，甚至栈溢出；调整这些选项的值时请务必谨慎。
选项
pp.maxSteps
默认值：5000
（美化打印器）访问表达式的最大次数；超过后将项打印为 ⋯。默认值为 5000。
14.2.2. 元变量
以问号开头的项是元变量，对应某个未知值。
它们既可以代表宇宙层级，也可以代表项。
有些元变量产生于 Lean 的精译过程，即现有信息尚不足以确定某个值之时。
这些元变量名称的末尾带有数字部分，例如 ?m.392 或 ?u.498。
其他元变量则由策略或合成孔洞产生。
这些元变量的名称不带数字部分。
由策略产生的元变量经常表现为目标，其分支标签与元变量名称一致。
证明中的元变量
显式创建的元变量
可以使用选项 pp.mvars 禁用元变量编号的显示。
使用 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档
注释的内容匹配。
基本示例：
```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```
这会检查确有此错误，然后消费该消息。
默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告：
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
或只选择错误：
```lean
#guard_msgs(error) in
example : α := sorry
```
在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告：
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句：
```
#guard_msgs (configElt,*) in cmd
```
默认配置列表为
`(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。
消息过滤器按严重程度选择消息：
- `info`、`warning`、`error`：具有相应严重程度的非跟踪消息；
- `trace`：跟踪消息；
- `all`：所有消息。
过滤器可带有指定操作的前缀：
- `check`（默认）：捕获并检查消息；
- `drop`：丢弃消息；
- `pass`：让消息继续传递。
若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式
添加 `pass all`。
空白处理（先去除开头和末尾的空白）：
- `whitespace := exact` 要求空白完全匹配；
- `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行；
- `whitespace := lax` 在匹配前把连续空白压缩为一个空格。
消息排序：
- `ordering := exact` 使用消息的原始顺序（默认）；
- `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。
位置信息：
- `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围；
- `positions := false` 不报告位置信息。
子串匹配：
- `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心
消息一部分的情况；
- `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。
稳定输出：
消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。
使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留
`?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为
`?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的
松散自由变量名替换为 `_fvar._`。
例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。
命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码
检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令
运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。
因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 这类将 Lean 输出与预期字符串匹配的功能时，这一点很有用；这类功能对于编写自定义策略测试尤为有用。