7.1. 修饰符🔗

声明支持一组一致的 修饰符，它们均为可选。 修饰符会改变声明在解释上的某些方面；例如可以添加文档，或改变其作用域。 修饰符的顺序是固定的，但并非所有种类的声明都接受所有种类的修饰符。

declModifiers ::=
    `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。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?
    attributes?
    visibility?
    noncomputable?
    unsafe?
    (partial | nonrec)?

文档注释用于为它所修饰的声明提供源码内 API 文档。 文档注释实际上并不是普通注释：把它放在不会被当作文档处理的位置会造成语法错误。 它也用于需要文本、但字符串转义会很繁琐的位置，例如 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 命令中的预期消息。

docComment ::=
    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.
/--
    ...
    -/

属性是可扩展的一类修饰符，用于将附加信息关联到声明上。 它们在 属性专章中有详细说明。

若声明被标记为 private，则无法在其定义所在模块之外访问。 若声明为 protected，则打开其命名空间时不会将该名字带入作用域。

被标记为 noncomputable 的函数不会被编译，因而也不能执行。 当函数使用了非可计算的推理原则（例如选择公理或排中律）来产生与其返回结果相关的数据，或使用了因效率原因而不参与代码生成的 Lean 特性（如 递归器）时，该函数必须是 noncomputable。 即使无法编译和执行，noncomputable 函数在规范化与推理中依然十分有用。

unsafe 标记会使定义跳过内核检查，并允许其访问可能破坏 Lean 保证的功能。 使用该标记务必小心，仅在深入理解 Lean 内部机制时使用。