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

missing : Lean.Syntax

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

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

ident (info : Lean.SourceInfo) (rawVal : Substring)
  (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

«namespace» (ns : Lean.Name) : 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.

`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

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

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

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

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.

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

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.

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.

Declares a new syntactic category.

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.

A `docComment` 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. 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 flexiblity 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

default : Lean.Parser.LeadingIdentBehavior

symbol : 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.

A `docComment` 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. 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

The syntactic category stx is the grammar of specifiers that may occur in the body of a Lean.Parser.Command.syntax : commandsyntax command.

String literals are parsed as atoms (including both keywords such as if, #eval, or where):

stx ::=
    str

Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntax in proof states and error messages. Ordinarily, valid identifiers occurring as atoms in syntax rules become reserved keywords. Preceding a string literal with an ampersand (&) suppresses this behavior:

stx ::= ...
    | &str

Identifiers specify the syntactic category expected in a given position, and may optionally provide a precedence:

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

The * modifier is the Kleene star, matching zero or more repetitions of the preceding syntax. It can also be written using 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 *

The + modifier matches one or more repetitions of the preceding syntax. It can also be written using 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 +

The ? modifier makes a subterm optional, and matches zero or one, but not more, repetitions of the preceding syntax. It can also be written as 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)

The ,* modifier matches zero or more repetitions of the preceding syntax with interleaved commas. It can also be written using 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 ,*

The ,+ modifier matches one or more repetitions of the preceding syntax with interleaved commas. It can also be written using sepBy1.

stx ::= ...
    | `p,+` is shorthand for `sepBy(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 ,+

The ,*,? modifier matches zero or more repetitions of the preceding syntax with interleaved commas, allowing an optional trailing comma after the final repetition. It can also be written using sepBy with the allowTrailingSep modifier.

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 ,*,?

The ,+,? modifier matches one or more repetitions of the preceding syntax with interleaved commas, allowing an optional trailing comma after the final repetition. It can also be written using sepBy1 with the allowTrailingSep modifier.

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 ,+,?

The <|> operator, which can be written orelse, matches either syntax. However, if the first branch consumes any tokens, then it is committed to, and failures will not be backtracked:

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)

The ! operator matches the complement of its argument. If its argument fails, then it succeeds, resetting the parsing state.

stx ::= ...
    | `!p` parses the negation of `p`. That is, it fails if `p` succeeds, and
otherwise parses nothing. It has arity 0.
! stx

Syntax specifiers may be grouped using parentheses.

stx ::= ...
    | (stx)

Repetitions may be defined using many and many1. The latter requires at least one instance of the repeated syntax.

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

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

Repetitions with separators may be defined using sepBy and sepBy1, which respectively match zero or more occurrences and one or more occurrences, separated by some other syntax. They come in three varieties:

• The two-parameter version uses the atom provided in the string literal to parse the separators, and does not allow trailing separators.

• The three-parameter version uses the third parameter to parse the separators, using the atom for pretty-printing.

• The four-parameter version optionally allows the separator to occur an extra time at the end of the sequence. The fourth argument must always literally be the keyword 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.