Lean syntax trees.

Syntax trees are used pervasively throughout Lean: they are produced by the parser, transformed by the macro expander, and elaborated. They are also produced by the delaborator and presented to users.

Constructors

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

A possible binding of an identifier in the context in which it was quoted.

Identifiers in quotations may refer to either global declarations or to namespaces that are in scope at the site of the quotation. These are saved in the Syntax.ident constructor and are part of the implementation of hygienic macros.

Constructors

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

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

Specifies the interpretation of a Syntax.node value. An abbreviation for Name.

Node kinds may be any name, and do not need to refer to declarations in the environment. Conventionally, however, a node's kind corresponds to the Parser or ParserDesc declaration that produces it. There are also a number of built-in node kinds that are used by the parsing infrastructure, such as nullKind and choiceKind; these do not correspond to parser declarations.

Checks whether syntax has the given kind or pseudo-kind.

“Pseudo-kinds” are kinds that are assigned by convention to non-Syntax.node values: identKind for Syntax.ident, `missing for Syntax.missing, and the atom's string literal for atoms.

Gets the kind of a Syntax.node value, or the pseudo-kind of any other Syntax value.

“Pseudo-kinds” are kinds that are assigned by convention to non-Syntax.node values: identKind for Syntax.ident, `missing for Syntax.missing, and the atom's string literal for atoms.

Changes the kind at the root of a Syntax.node to k.

Returns all other Syntax values unchanged.

The pseudo-kind assigned to identifiers: `ident.

The name `ident is not actually used as a kind for Syntax.node values. It is used by convention as the kind of Syntax.ident values.

`str is the node kind of string literals like "foo".

`interpolatedStrKind is the node kind of an interpolated string literal like "value = {x}" in s!"value = {x}".

`interpolatedStrLitKind is the node kind of interpolated string literal fragments like "value = { and }" in s!"value = {x}".

`char is the node kind of character literals like 'A'.

`num is the node kind of number literals like 42 and 0xa1

`scientific is the node kind of floating point literals like 1.23e-3.

`name is the node kind of name literals like `foo.

`fieldIdx is the node kind of projection indices like the 2 in x.2.

The `group kind is used for nodes that result from Lean.Parser.group. This avoids confusion with the null kind when used inside optional.

`null is the “fallback” kind, used when no other kind applies. Null nodes result from repetition operators, and empty null nodes represent the failure of an optional parse.

The null kind is used for raw list parsers like many.

The `choice kind is used to represent ambiguous parse results.

The parser prioritizes longer matches over shorter ones, but there is not always a unique longest match. All the parse results are saved, and the determination of which to use is deferred until typing information is available.

`hygieneInfo is the node kind of the Lean.Parser.hygieneInfo parser, which produces an “invisible token” that captures the hygiene information at the current point without parsing anything.

They can be used to generate identifiers (with Lean.HygieneInfo.mkIdent) as if they were introduced in a macro's input, rather than by its implementation.

Source information that relates syntax to the context that it came from.

The primary purpose of SourceInfo is to relate the output of the parser and the macro expander to the original source file. When produced by the parser, Syntax.node does not carry source info; the parser associates it only with atoms and identifiers. If a Syntax.node is introduced by a quotation, then it has synthetic source info that both associates it with an original reference position and indicates that the original atoms in it may not originate from the Lean file under elaboration.

Source info is also used to relate Lean's output to the internal data that it represents; this is the basis for many interactive features. When used this way, it can occur on Syntax.node as well.

Constructors

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

Typed syntax, which tracks the potential kinds of the Syntax it contains.

While syntax quotations produce or expect TSyntax values of the correct kinds, this is not otherwise enforced; it can easily be circumvented by direct use of the constructor.

Constructor

Lean.TSyntax.mk

Fields

raw : Lean.Syntax

SyntaxNodeKinds is a set of SyntaxNodeKind, implemented as a list.

Singleton SyntaxNodeKinds are extremely common. They are written as name literals, rather than as lists; list syntax is required only for empty or non-singleton sets of kinds.

An array of syntaxes of kind ks.

Converts a TSyntaxArray to an Array Syntax, without reallocation.

An array of syntax elements that alternate with the given separator. Each syntax element has a kind drawn from ks.

Separator arrays result from repetition operators such as ,*. Coercions to and from Array (TSyntax ks) insert or remove separators as required. The untyped equivalent is Lean.Syntax.SepArray.

Constructor

Lean.Syntax.TSepArray.mk

Fields

elemsAndSeps : Array Lean.Syntax

Extracts the non-separator elements of a separated array.

The array of elements and separators, ordered like #[el1, sep1, el2, sep2, el3].

Constructs a typed separated array from elements by adding suitable separators. The provided array should not include the separators.

Like Syntax.SepArray.ofElems but for typed syntax.

Adds an element to the end of a separated array, adding a separator as needed.

Syntax that represents a Lean term.

Syntax that represents a command.

Syntax that represents a universe level.

Syntax that represents a tactic.

Syntax that represents a precedence (e.g. for an operator).

Syntax that represents a priority (e.g. for an instance declaration).

Syntax that represents an identifier.

Syntax that represents a string literal.

Syntax that represents a character literal.

Syntax that represents a quoted name literal that begins with a back-tick.

Syntax that represents a numeric literal.

Syntax that represents a scientific numeric literal that may have decimal and exponential parts.

Syntax that represents macro hygiene info.

Creates an identifier from a name. The resulting identifier has no source position.

Creates an identifier with its position copied from src.

To refer to a specific constant without a risk of variable capture, use mkCIdentFrom instead.

Creates an identifier with its position copied from the syntax returned by getRef.

To refer to a specific constant without a risk of variable capture, use mkCIdentFromRef instead.

Creates an identifier that refers to a constant c. The identifier has no source position.

This variant of mkIdent makes sure that the identifier cannot accidentally be captured.

Creates an identifier referring to a constant c. The identifier's position is copied from src.

This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

Creates an identifier referring to a constant c. The identifier's position is copied from the syntax returned by getRef.

This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

Creates syntax representing a Lean term application, but avoids degenerate empty applications.

Creates syntax representing a Lean constant application, but avoids degenerate empty applications.

Creates a literal of the given kind. It is the caller's responsibility to ensure that the provided literal is a valid atom for the provided kind.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for the given character.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for the given string.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for a number, which is provided as a string. The caller must ensure that the string is a valid token for the num token parser.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for a natural number.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for a number in scientific notation. The caller must ensure that the provided string is a valid scientific notation literal.

If info is provided, then the literal's source information is copied from it.

Creates literal syntax for a name. The caller must ensure that the provided string is a valid name literal.

If info is provided, then the literal's source information is copied from it.

Creates an optional node.

Optional nodes consist of null nodes that contain either zero or one element.

Creates a group node, as if it were parsed by Lean.Parser.group.

Creates a hole (_). The hole's position is copied from ref.

Extracts the parsed name from the syntax of an identifier.

Returns Name.anonymous if the syntax is malformed.

Decodes a quoted name literal, returning the name.

Returns Lean.Name.anonymous if the syntax is malformed.

Interprets a numeric literal as a natural number.

Returns 0 if the syntax is malformed.

Extracts the components of a scientific numeric literal.

Returns a triple (n, sign, e) : Nat × Bool × Nat; the number's value is given by:

Returns (0, false, 0) if the syntax is malformed.

Decodes a string literal, removing quotation marks and unescaping escaped characters.

Returns "" if the syntax is malformed.

Decodes a character literal.

Returns (default : Char) if the syntax is malformed.

Decodes macro hygiene information.

声明一个新的语法类别。

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?
      declare_syntax_cat ident ((behavior := (catBehaviorBoth | catBehaviorSymbol)))?

Specifies how the parsing table lookup function behaves for identifiers.

The function Lean.Parser.prattParser uses two tables: one each for leading and trailing parsers. These tables map tokens to parsers. Because keyword tokens are distinct from identifier tokens, keywords and identifiers cannot be confused, even when they are syntactically identical. Specifying an alternative leading identifier behavior allows greater flexibility and makes it possible to avoid reserved keywords in some situations.

When the leading token is syntactically an identifier, the current syntax category's LeadingIdentBehavior specifies how the parsing table lookup function behaves, and allows controlled “punning” between identifiers and keywords. This feature is used to avoid creating a reserved symbol for each built-in tactic (e.g., apply or assumption). As a result, tactic names can be used as identifiers.

Constructors

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

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

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

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
      syntax(:prec)? ((name := ident))? ((priority := prio))? `p*` is shorthand for `many(p)`. It uses parser `p` 0 or more times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

If `p` has arity more than 1, it is auto-grouped in the items generated by the parser.
stx* : ident

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

字符串文字被解析为 atoms（包括 if、#eval 或 where 等关键字）：

stx ::=
    Parses the literal symbol.

The symbol is automatically included in the set of reserved tokens ("keywords").
Keywords cannot be used as identifiers, unless the identifier is otherwise escaped.
For example, `"fun"` reserves `fun` as a keyword; to refer an identifier named `fun` one can write `«fun»`.
Adding a `&` prefix prevents it from being reserved, for example `&"true"`.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.
str

字符串中的前导空格和尾随空格不会影响解析，但会导致 Lean 在显示 proof states 中的语法和错误消息时在相应位置插入空格。 通常，在语法规则中作为原子出现的有效标识符成为保留关键字。 在字符串文字前面加上 & 符号 (&) 可抑制此行为：

stx ::= ...
    | Parses a literal symbol. The `&` prefix prevents it from being included in the set of reserved tokens ("keywords").
This means that the symbol can still be recognized as an identifier by other parsers.

Some syntax categories, such as `tactic`, automatically apply `&` to the first symbol.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.

(Not exposed by parser description syntax:
If the `includeIdent` argument is true, lets `ident` be reinterpreted as `atom` if it matches.)
&str

标识符指定给定位置预期的语法类别，并且可以选择提供优先级：

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

* 修饰符是 Kleene 星号，匹配前面语法的零次或多次重复。 也可以使用 many 写入。

stx ::= ...
    | `p*` is shorthand for `many(p)`. It uses parser `p` 0 or more times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

If `p` has arity more than 1, it is auto-grouped in the items generated by the parser.
stx *

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

stx ::= ...
    | `p+` is shorthand for `many1(p)`. It uses parser `p` 1 or more times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

If `p` has arity more than 1, it is auto-grouped in the items generated by the parser.
stx +

? 修饰符使子项成为可选，并匹配前面语法的零次或一次（但不能多次）重复。 也可写为optional。

stx ::= ...
    | `(p)?` is shorthand for `optional(p)`. It uses parser `p` 0 or 1 times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

`p` is allowed to have arity n > 1 (in which case the node will have either 0 or n children),
but if it has arity 0 then the result will be ambiguous.

Because `?` is an identifier character, `ident?` will not work as intended.
You have to write either `ident ?` or `(ident)?` for it to parse as the `?` combinator
applied to the `ident` parser.
stx ?

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

,* 修饰符与前面带有交错逗号的语法的零次或多次重复相匹配。 也可以使用 sepBy 写入。

stx ::= ...
    | `p,*` is shorthand for `sepBy(p, ",")`. It parses 0 or more occurrences of
`p` separated by `,`, that is: `empty | p | p,p | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
stx ,*

,+ 修饰符与前面带有交错逗号的语法的一次或多次重复相匹配。 也可以使用 sepBy1 写入。

stx ::= ...
    | `p,+` is shorthand for `sepBy1(p, ",")`. It parses 1 or more occurrences of
`p` separated by `,`, that is: `p | p,p | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
stx ,+

,*,? 修饰符将前面语法的零次或多次重复与交错逗号匹配，从而允许在最终重复之后使用可选的尾随逗号。 也可以使用 sepBy 和 allowTrailingSep 修饰符来编写。

stx ::= ...
    | `p,*,?` is shorthand for `sepBy(p, ",", allowTrailingSep)`.
It parses 0 or more occurrences of `p` separated by `,`, possibly including
a trailing `,`, that is: `empty | p | p, | p,p | p,p, | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
stx ,*,?

,+,? 修饰符将前面语法的一次或多次重复与交错逗号相匹配，从而允许在最后一次重复之后使用可选的尾随逗号。 也可以使用 sepBy1 和 allowTrailingSep 修饰符来编写。

stx ::= ...
    | `p,+,?` is shorthand for `sepBy1(p, ",", allowTrailingSep)`.
It parses 1 or more occurrences of `p` separated by `,`, possibly including
a trailing `,`, that is: `p | p, | p,p | p,p, | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
stx ,+,?

<|> 运算符（可写为 orelse）与任一语法匹配。 然而，如果第一个分支消耗了任何令牌，那么它就会被提交，并且失败将不会被回溯：

stx ::= ...
    | `p1 <|> p2` is shorthand for `orelse(p1, p2)`, and parses either `p1` or `p2`.
It does not backtrack, meaning that if `p1` consumes at least one token then
`p2` will not be tried. Therefore, the parsers should all differ in their first
token. The `atomic(p)` parser combinator can be used to locally backtrack a parser.
(For full backtracking, consider using extensible syntax classes instead.)

On success, if the inner parser does not generate exactly one node, it will be
automatically wrapped in a `group` node, so the result will always be arity 1.

The `<|>` combinator does not generate a node of its own, and in particular
does not tag the inner parsers to distinguish them, which can present a problem
when reconstructing the parse. A well formed `<|>` parser should use disjoint
node kinds for `p1` and `p2`.
stx <|> stx

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

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

stx ::= ...
    | `!p` parses the negation of `p`. That is, it fails if `p` succeeds, and
otherwise parses nothing. It has arity 0.
! 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)

Arity is sum of arguments' arities

withPosition(p) runs p while setting the "saved position" to the current position. This has no effect on its own, but various other parsers access this position to achieve some composite effect:

• colGt, colGe, colEq compare the column of the saved position to the current position, used to implement Python-style indentation sensitive blocks

• lineEq ensures that the current position is still on the same line as the saved position, used to implement composite tokens

The saved position is only available in the read-only state, which is why this is a scoping parser: after the withPosition(..) block the saved position will be restored to its original value.

This parser has the same arity as p - it just forwards the results of p.

Arity is sum of arguments' arities

withoutPosition(p) runs p without the saved position, meaning that position-checking parsers like colGt will have no effect. This is usually used by bracketing constructs like (...) so that the user can locally override whitespace sensitivity.

This parser has the same arity as p - it just forwards the results of p.

• Arity: 1
• Automatically wraps arguments in a null node unless there's exactly one

• Arity: 0
• Automatically wraps arguments in a null node unless there's exactly one

The colGt parser requires that the next token starts a strictly greater column than the saved position (see withPosition). This can be used for whitespace sensitive syntax for the arguments to a tactic, to ensure that the following tactic is not interpreted as an argument.

example (x : False) : False := by
  revert x
  exact id

Here, the revert tactic is followed by a list of colGt ident, because otherwise it would interpret exact as an identifier and try to revert a variable named exact.

This parser has arity 0 - it does not capture anything.

• Arity: 0
• Automatically wraps arguments in a null node unless there's exactly one

The colGe parser requires that the next token starts from at least the column of the saved position (see withPosition), but allows it to be more indented. This can be used for whitespace sensitive syntax to ensure that a block does not go outside a certain indentation scope. For example it is used in the lean grammar for else if, to ensure that the else is not less indented than the if it matches with.

This parser has arity 0 - it does not capture anything.

• Arity: 0
• Automatically wraps arguments in a null node unless there's exactly one

The colEq parser ensures that the next token starts at exactly the column of the saved position (see withPosition). This can be used to do whitespace sensitive syntax like a by block or do block, where all the lines have to line up.

This parser has arity 0 - it does not capture anything.

• Arity: 0
• Automatically wraps arguments in a null node unless there's exactly one

The lineEq parser requires that the current token is on the same line as the saved position (see withPosition). This can be used to ensure that composite tokens are not "broken up" across different lines. For example, else if is parsed using lineEq to ensure that the two tokens are on the same line.

This parser has arity 0 - it does not capture anything.