23.3. 符号🔗

术语 notation 在 Lean 中有两种使用方式：它可以指以简洁的方式记录想法的一般概念，它是允许用很少的代码方便地实现符号的语言功能的名称。 与自定义运算符一样，Lean 符号允许使用新形式扩展术语语法。 然而，符号更加通用：新语法可以自由地将所需的关键字或运算符与子术语混合在一起，并且它们提供对优先级的更精确的控制。 符号还可以在结果子项中重新排列它们的参数，而中缀运算符以固定顺序将它们提供给函数项。 由于符号可以定义混合使用前缀、中缀和后缀组件的运算符，因此它们可以称为 mixfix 运算符。

command ::= ...
    | 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?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind notation(:prec)? ((name := ident))? ((priority := prio))? notationItem* => term

notationItem ::=
    str

notationItem ::= ...
    | ident(:prec)?

与运算符声明一样，当用户与新语法交互时，会向用户显示文档注释的内容。 添加 inherit_doc 属性会导致符号扩展到的术语开头的函数文档注释被复制到新语法。 可以添加其他属性以在结果定义上调用其他编译时元程序。

符号与 节范围 的交互方式与属性和运算符相同。 默认情况下，符号在任何可传递导入建立符号的模块中都可用，但它们可以声明为 scoped 或 local，以分别将其可用性限制在当前名称空间已打开的上下文或当前 节范围 中。

与运算符一样，解析符号时使用 本地最长匹配规则。 如果最长匹配有多个表示法，则使用声明的优先级来确定应用哪个解析结果。 如果这仍然不能解决歧义，则所有内容都会被保存，并且精化器预计会尝试所有这些内容，当恰好有一个可以详细说明时就会成功。

符号声明的主体不是由具有固定性和标记的单个运算符组成，而是由一系列 notation items 组成，它可以是新的 atoms（包括 if、#eval 或 where 等关键字和符号，例如=>、+、↗、⟦ 或 ⋉）或条款的位置。 正如它们在运算符中所做的那样，字符串文字标识原子的位置。 字符串中的前导空格和尾随空格不会影响解析，但会导致 Lean 在显示 proof states 中的语法和错误消息时在相应位置插入空格。 标识符指示需要术语的位置，并命名相应的术语，以便可以将其插入符号的扩展中。

虽然自定义运算符只有一个优先级概念，但符号中涉及很多内容。 符号本身具有优先级，每个要解析的术语也具有优先级。 符号的优先级决定了它可以在哪些上下文中进行解析：解析器仅尝试解析优先级至少与当前上下文一样高的产生式。 例如，由于乘法的优先级高于加法，因此解析器将在解析加法参数时尝试解析中缀乘法项，但反之则不然。 要解析的每个术语的优先级决定了其中可能出现哪些其他产生式。

如果没有为符号本身提供优先级，则默认值取决于符号的形式。 如果表示法均以原子开头和结尾（由字符串文字表示），则默认优先级为 max. 这既适用于仅由单个原子组成的符号，也适用于具有多个项目的符号，其中第一个和最后一个项目都是原子。 否则，整个表示法的默认优先级是 lead。 如果没有为作为术语的符号项目提供优先级，则它们默认为优先级 min。

在所需的双箭头（Lean.Parser.Command.notation : command=>）之后，提供了扩展符号。 虽然运算符总是通过按顺序将其函数应用于运算符的参数来扩展，但符号可以将其术语项放置在扩展中的任何位置。 这些术语通过名称来引用。 术语项可以在扩展中出现任意多次。 由于符号扩展是在精化或代码生成之前发生的纯粹语法过程，因此扩展中的重复项可能会导致在计算结果项时出现重复计算，甚至在 monad 中工作时出现重复的副作用。

5

#eval ignore (2 +unexpected token ')'; expected term) 5

<example>:1:17-1:18: unexpected token ')'; expected term

def e : Nat × Int :=
(2 + 2, 2 + 2)

当扩展由全局环境中定义的函数的应用组成并且符号中的每个项恰好出现一次时，会生成 unexpander。 当匹配函数应用术语时，新符号将显示在 证明状态、错误消息和 Lean 的其他输出中，否则会显示。 与自定义运算符一样，Lean 不会跟踪原始术语中是否使用了该符号；它在 Lean 输出中的每个机会都使用。

fun x => decide (x > 5) && decide (x < 8) : Nat → Bool

[5 ⇒' 8] : Nat → Prop