Lean 的语法树。

语法树在 Lean 中无处不在：解析器产生语法树，宏展开器变换语法树，精译器再精译 语法树。反精译器也会产生语法树，并把它们呈现给用户。

Lean.Syntax.missing : Lean.Syntax

Lean.Syntax.node (info : Lean.SourceInfo)
  (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) :
  Lean.Syntax

Lean.Syntax.atom (info : Lean.SourceInfo) (val : String) :
  Lean.Syntax

Lean.Syntax.ident (info : Lean.SourceInfo)
  (rawVal : Substring.Raw) (val : Lean.Name)
  (preresolved : List Lean.Syntax.Preresolved) : Lean.Syntax

标识符在被引用位置的上下文中可能指向的绑定。

引用中的标识符既可能指向全局声明，也可能指向引用处作用域内的命名空间。这些信息 保存在 Syntax.ident 构造子中，是卫生宏实现的一部分。

Lean.Syntax.Preresolved.namespace (ns : Lean.Name) :
  Lean.Syntax.Preresolved

Lean.Syntax.Preresolved.decl (n : Lean.Name)
  (fields : List String) : Lean.Syntax.Preresolved

指定 Syntax.node 值的解释；它是 Name 的缩写。

节点种类可以是任意名称，不必指向环境中的声明。不过按照约定，节点种类通常对应于 生成它的 Parser 或 ParserDesc 声明。解析基础设施还使用若干不对应解析器声明的 内建种类，例如 nullKind 和 choiceKind。

检查语法是否具有给定的种类或伪种类。

“伪种类”是按约定赋予非 Syntax.node 值的种类：Syntax.ident 使用 identKind， Syntax.missing 使用 `missing，原子使用其字符串字面量。

取得 Syntax.node 的种类，或其他 Syntax 值的伪种类。

“伪种类”是按约定赋予非 Syntax.node 值的种类：Syntax.ident 使用 identKind， Syntax.missing 使用 `missing，原子使用其字符串字面量。

把 Syntax.node 根部的种类改为 k。

所有其他 Syntax 值均原样返回。

赋予标识符的伪种类：`ident。

名称 `ident 实际上并不用作 Syntax.node 值的种类；按约定，它用作 Syntax.ident 值的种类。

`str 是字符串字面量（如 "foo"）的节点种类。

`interpolatedStrKind 是 s!"value = {x}" 中 "value = {x}" 这类插值字符串 字面量的节点种类。

`interpolatedStrLitKind 是 s!"value = {x}" 中 "value = { 和 }" 这类插值 字符串字面量片段的节点种类。

`char 是字符字面量（如 'A'）的节点种类。

`num 是数字字面量（如 42 和 0xa1）的节点种类。

`scientific 是科学计数法浮点字面量（如 1.23e-3）的节点种类。

`name 是名称字面量（如 `foo）的节点种类。

`fieldIdx 是投影索引（如 x.2 中的 2）的节点种类。

`group 用于 Lean.Parser.group 产生的节点，避免其在 optional 内与空种类混淆。

`null 是没有其他种类适用时的后备种类。重复运算符会产生空节点，而空的空节点 表示可选解析失败。

many 等原始列表解析器使用空种类。

`choice 种类用于表示有歧义的解析结果。

解析器优先选择更长的匹配，但最长匹配并不总是唯一的。所有解析结果都会保存起来， 直到有类型信息时再决定使用哪一个。

`hygieneInfo 是 Lean.Parser.hygieneInfo 的节点种类。该解析器不消耗输入，却产生 捕获当前位置卫生信息的“不可见记号”。

它们可通过 Lean.HygieneInfo.mkIdent 生成仿佛由宏输入而非宏实现引入的标识符。

把语法与其来源上下文关联起来的源信息。

SourceInfo 的主要用途是把解析器和宏展开器的输出关联到原始源文件。解析器产生的 Syntax.node 通常不携带源信息；解析器只把源信息附在原子和标识符上。引用产生的 Syntax.node 则带有合成源信息，既把它关联到一个原始参考位置，也表明其中的原始 原子可能并非来自当前正在精译的 Lean 文件。

源信息还用于把 Lean 的输出关联到其所表示的内部数据，这是许多交互功能的基础。 在这种用途下，Syntax.node 也可以携带源信息。

Lean.SourceInfo.original (leading : Substring.Raw)
  (pos : String.Pos.Raw) (trailing : Substring.Raw)
  (endPos : String.Pos.Raw) : Lean.SourceInfo

Lean.SourceInfo.synthetic (pos endPos : String.Pos.Raw)
  (canonical : Bool := false) : Lean.SourceInfo

`(if $h : $cond then $t else $e) ~>
`(dite $cond (fun $h => $t) (fun $h => $t))

Lean.SourceInfo.none : Lean.SourceInfo

带类型语法；它跟踪其中 Syntax 可能具有的种类。

语法引用会产生或要求种类正确的 TSyntax，但除此之外并无强制保证；直接使用构造子 即可轻易绕过这一约束。

Lean.TSyntax.mk

raw : Lean.Syntax

SyntaxNodeKinds 是用列表实现的 SyntaxNodeKind 集合。

单元素 SyntaxNodeKinds 极为常见，可直接写成名称字面量而不是列表；只有空集合或 多元素种类集合才需要列表语法。

某一种类集合 ks 的带类型语法数组。

不重新分配内存，把 TSyntaxArray 转换成 Array Syntax。

由给定分隔符交错分隔的带类型语法数组；每个语法元素的种类来自 ks。

分隔数组由 ,* 等重复运算符产生。强制转换 到 Array (TSyntax ks) 或从中转换时，会按需插入或移除分隔符。无类型版本是 Lean.Syntax.SepArray。

Lean.Syntax.TSepArray.mk

elemsAndSeps : Array Lean.Syntax

从分隔数组中提取所有非分隔符元素。

元素与分隔符按 #[el1, sep1, el2, sep2, el3] 的顺序排列。

从元素构造带类型分隔数组，并添加适当的分隔符。所提供的数组不应包含分隔符。

类似于 Syntax.SepArray.ofElems，但用于带类型语法。

在分隔数组末尾添加元素，并在需要时添加分隔符。

表示 Lean 项的语法。

表示命令的语法。

表示宇宙层级的语法。

表示策略的语法。

表示优先级（例如运算符优先级）的语法。

表示优先权（例如实例声明优先权）的语法。

表示标识符的语法。

表示字符串字面量的语法。

表示字符字面量的语法。

表示以反引号开头的名称字面量的语法。

表示数字字面量的语法。

表示可含小数部分和指数部分的科学计数法数字字面量的语法。

表示宏卫生信息的语法。

从名称创建标识符。所得标识符没有源位置。

创建标识符，其位置从 src 复制。

若要无变量捕获风险地指向特定常量，请改用 mkCIdentFrom。

创建标识符，其位置从 getRef 返回的语法复制。

若要无变量捕获风险地指向特定常量，请改用 mkCIdentFromRef。

创建指向常量 c 的标识符。该标识符没有源位置。

此 mkIdent 变体确保标识符不会意外被捕获。

创建指向常量 c 的标识符。该标识符的位置从 src 复制。

此 mkIdentFrom 变体确保标识符不会意外被捕获。

创建指向常量 c 的标识符。该标识符的位置从 getRef 返回的语法复制。

此 mkIdentFrom 变体确保标识符不会意外被捕获。

创建表示 Lean 项应用的语法，同时避免产生退化的空应用。

创建表示 Lean 常量应用的语法，同时避免产生退化的空应用。

创建给定种类的字面量。调用者负责确保所提供的字面量是该种类的合法原子。

若提供 info，则从中复制字面量的源信息。

为给定字符创建字面量语法。

若提供 info，则从中复制字面量的源信息。

为给定字符串创建字面量语法。

若提供 info，则从中复制字面量的源信息。

为以字符串提供的数字创建字面量语法。调用者必须确保该字符串是 num 记号解析器的 合法记号。

若提供 info，则从中复制字面量的源信息。

为自然数创建字面量语法。

若提供 info，则从中复制字面量的源信息。

为科学计数法数字创建字面量语法。调用者必须确保所提供的字符串是合法的科学计数法 字面量。

若提供 info，则从中复制字面量的源信息。

为名称创建字面量语法。调用者必须确保所提供的字符串是合法的名称字面量。

若提供 info，则从中复制字面量的源信息。

创建可选节点。

可选节点是包含零个或一个元素的空种类节点。

创建仿佛由 Lean.Parser.group 解析得到的分组节点。

创建空洞（_），并从 ref 复制空洞的位置。

从标识符语法中提取解析后的名称。

若语法畸形，则返回 Name.anonymous。

解码带反引号的名称字面量并返回名称。

若语法畸形，则返回 Lean.Name.anonymous。

把数字字面量解释为自然数。

若语法畸形，则返回 0。

提取科学计数法数字字面量的组成部分。

返回三元组 (n, sign, e) : Nat × Bool × Nat；该数字的值为：

若语法畸形，则返回 (0, false, 0)。

解码字符串字面量，去掉引号并反转义转义字符。

若语法畸形，则返回 ""。

解码字符字面量。

若语法畸形，则返回 (default : Char)。

解码宏卫生信息。

声明一个新的语法类别。

command ::= ...
    | docComment?
      declare_syntax_cat ident ((behavior := (catBehaviorBoth | catBehaviorSymbol)))?

指定解析表查询函数在遇到标识符时的行为。

Lean.Parser.prattParser 分别用一张表保存前导解析器和尾随解析器；表把记号映射到解析器。 关键字记号与标识符记号不同，故即使拼写相同也不会混淆。替代的前导标识符行为提供了 更大的灵活性，使某些场景可以避免保留关键字。

当前导记号在语法上是标识符时，当前语法类别的 LeadingIdentBehavior 控制解析表查询， 允许在标识符和关键字之间进行受控的双关。这用于避免为每个内建策略（如 apply 或 assumption）都创建保留符号，从而让策略名称仍可用作标识符。

Lean.Parser.LeadingIdentBehavior.default :
  Lean.Parser.LeadingIdentBehavior

Lean.Parser.LeadingIdentBehavior.symbol :
  Lean.Parser.LeadingIdentBehavior

Lean.Parser.LeadingIdentBehavior.both :
  Lean.Parser.LeadingIdentBehavior

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind
      syntax(:prec)? ((name := ident))? ((priority := prio))? stx* : ident

语法类别 stx 是可出现在 Lean.Parser.Command.syntax : commandsyntax 命令主体中的说明符语法。

字符串字面量会被解析为 原子（包括 if、#eval、where 等关键字）：

stx ::=
    str

字符串中的前导和尾随空格不会影响解析，但在 Lean 的 证明状态 和错误消息中显示该语法时，它们会使 Lean 在相应位置插入空格。 通常，在语法规则中作为原子出现的合法标识符会变成保留关键字。 如果在字符串字面量前加上一个和号（&），就会抑制这一行为：

stx ::= ...
    | &str

标识符指定给定位置上期望的语法类别，并且可以选择性地提供一个优先级：

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

* 修饰符是克林星号，用于匹配前述语法的零次或多次重复。 它也可以写作 many。

stx ::= ...
    | stx *

+ 修饰符匹配前述语法的一次或多次重复。 它也可以写作 many1。

stx ::= ...
    | stx +

? 修饰符会让子项变为可选，它匹配前述语法的零次或一次重复，但不能更多。 它也可以写作 optional。

stx ::= ...
    | stx ?

stx ::= ...
    | optional(stx)

,* 修饰符匹配前述语法的零次或多次重复，并在其间穿插逗号。 它也可以写作 sepBy。

stx ::= ...
    | stx ,*

,+ 修饰符匹配前述语法的一次或多次重复，并在其间穿插逗号。 它也可以写作 sepBy1。

stx ::= ...
    | stx ,+

,*,? 修饰符匹配前述语法的零次或多次重复，并在其间穿插逗号，同时允许在最后一次重复后再跟一个可选尾随逗号。 它也可以通过带 allowTrailingSep 修饰符的 sepBy 来书写。

stx ::= ...
    | stx ,*,?

,+,? 修饰符匹配前述语法的一次或多次重复，并在其间穿插逗号，同时允许在最后一次重复后再跟一个可选尾随逗号。 它也可以通过带 allowTrailingSep 修饰符的 sepBy1 来书写。

stx ::= ...
    | stx ,+,?

<|> 运算符也可以写作 orelse，它匹配两边任一语法。 不过，如果第一条分支消耗了任何记号，那么解析就会提交到这条分支，之后失败也不会回溯：

stx ::= ...
    | stx <|> stx

stx ::= ...
    | orelse(stx, stx)

! 运算符匹配其参数的补集。 如果它的参数匹配失败，那么它就会成功，并重置解析状态。

stx ::= ...
    | ! stx

语法说明符可以用括号分组。

stx ::= ...
    | (stx)

重复也可以用 many 和 many1 来定义。 后者要求重复的语法至少出现一次。

stx ::= ...
    | many(stx)

stx ::= ...
    | many1(stx)

带分隔符的重复可以用 sepBy 和 sepBy1 来定义；它们分别匹配零次或多次出现，以及一次或多次出现，并由某种其他语法分隔。 它们有三种形式：

• 两参数版本使用字符串字面量中给出的原子来解析分隔符，并且不允许尾随分隔符。

• 三参数版本使用第三个参数来解析分隔符，而字符串原子只用于美化打印。

• 四参数版本可以选择性地允许分隔符在序列末尾额外再出现一次。 第四个参数必须字面上就是关键字 allowTrailingSep。

stx ::= ...
    | sepBy(stx, str)

stx ::= ...
    | sepBy(stx, str, stx)

stx ::= ...
    | sepBy(stx, str, stx, allowTrailingSep)

stx ::= ...
    | sepBy1(stx, str)

stx ::= ...
    | sepBy1(stx, str, stx)

stx ::= ...
    | sepBy1(stx, str, stx, allowTrailingSep)

参数元数是各实参元数之和。`withPosition(p)` 在运行 `p` 时把“已保存位置”设为当前位置。这本身不产生效果，但其他解析器会读取该位置以实现组合行为：`colGt`、`colGe` 和 `colEq` 将已保存位置的列与当前位置的列比较，用于实现类似 Python 的缩进敏感代码块；`lineEq` 确保当前位置仍与已保存位置处于同一行，用于实现复合词法单元。已保存位置只存在于只读状态中，因此这是一个定界解析器：离开 `withPosition(..)` 块后，已保存位置会恢复原值。此解析器与 `p` 的元数相同，只转发 `p` 的结果。

参数元数是各实参元数之和。`withoutPosition(p)` 在没有已保存位置的情况下运行 `p`，因此 `colGt` 等位置检查解析器不会生效。它通常用于 `(...)` 之类的括号结构，让用户能在局部关闭空白敏感性。此解析器与 `p` 的元数相同，只转发 `p` 的结果。

元数：1。除非恰好只有一个实参，否则自动用 `null` 节点包裹实参。

元数：0。除非恰好只有一个实参，否则自动用 `null` 节点包裹实参。解析器 `colGt` 要求下一个词法单元的起始列严格大于已保存位置的列（参见 `withPosition`）。它可用于策略实参等空白敏感语法，确保后续策略不会被解释成实参。示例中，`revert` 后接 `colGt ident` 列表；否则会把 `exact` 解释为标识符，并尝试回退名为 `exact` 的变量。此解析器元数为 0，不捕获任何内容。

元数：0。除非恰好只有一个实参，否则自动用 `null` 节点包裹实参。解析器 `colGe` 要求下一个词法单元的起始列不小于已保存位置的列（参见 `withPosition`），同时允许更深缩进。它可用于空白敏感语法，确保代码块不越出给定缩进作用域。例如，Lean 的 `else if` 语法用它保证 `else` 的缩进不小于与之匹配的 `if`。此解析器元数为 0，不捕获任何内容。

元数：0。除非恰好只有一个实参，否则自动用 `null` 节点包裹实参。解析器 `colEq` 确保下一个词法单元恰好从已保存位置所在列开始（参见 `withPosition`）。它可用于 `by` 块、`do` 块等空白敏感语法，其中各行必须对齐。此解析器元数为 0，不捕获任何内容。

元数：0。除非恰好只有一个实参，否则自动用 `null` 节点包裹实参。解析器 `lineEq` 要求当前词法单元与已保存位置位于同一行（参见 `withPosition`）。它可确保复合词法单元不会被换行拆开。例如，`else if` 使用 `lineEq` 解析，以确保两个词法单元位于同一行。此解析器元数为 0，不捕获任何内容。