Syntax objects used by the parser, macro expander, delaborator, etc.

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

Binding information resolved and stored at compile time of a syntax quotation. Note: We do not statically know whether a syntax expects a namespace or term name, so a Syntax.ident may contain both preresolution kinds.

Constructors

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

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

A SyntaxNodeKind classifies Syntax.node values. It is an abbreviation for Name, and you can use name literals to construct SyntaxNodeKinds, but they need not refer to declarations in the environment. Conventionally, a SyntaxNodeKind will correspond to the Parser or ParserDesc declaration that parses it.

Is this a syntax with node kind k?

Gets the kind of a Syntax node. For non-node syntax, we use "pseudo kinds": identKind for ident, missing for missing, and the atom's string literal for atoms.

Changes the kind at the root of a Syntax node to k. Does nothing for non-node nodes.

ident is not actually used as a node kind, but it is returned by getKind in the ident case so that things that handle different node kinds can also handle ident.

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 by the group parser, to avoid confusing with the null kind when used inside optional.

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

The choice kind is used when a piece of syntax has multiple parses, and the determination of which to use is deferred until typing information is available.

hygieneInfo is the node kind of the hygieneInfo parser, which is an "invisible token" which 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 by the calling context, not the called macro.

Source information of tokens.

Constructors

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

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

A Syntax value of one of the given syntax kinds. Note that while syntax quotations produce/expect TSyntax values of the correct kinds, this is not otherwise enforced and can easily be circumvented by direct use of the constructor. The namespace TSyntax.Compat can be opened to expose a general coercion from Syntax to any TSyntax ks for porting older code.

Constructor

Lean.TSyntax.mk

Fields

raw : Lean.Syntax

An array of syntaxes of kind ks.

A typed version of SepArray.

Constructor

Lean.Syntax.TSepArray.mk

Fields

elemsAndSeps : Array Lean.Syntax

新しい構文カテゴリを宣言します。

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)))?

The type LeadingIdentBehavior specifies how the parsing table lookup function behaves for identifiers. The function prattParser uses two tables leadingTable and trailingTable. They map tokens to parsers.

We use LeadingIdentBehavior.symbol and LeadingIdentBehavior.both and nonReservedSymbol parser to implement the tactic parsers. The idea is to avoid creating a reserved symbol for each builtin tactic (e.g., apply, assumption, etc.). That is, users may still use these symbols as identifiers (e.g., naming a function).

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

構文カテゴリ stx は Lean.Parser.Command.syntax : commandsyntax コマンドのボディに出現する可能性のある指定子についての文法です。

文字列リテラルは アトム （if・#eval・whereなどのキーワードを含む）としてパースされます：

stx ::=
    str

文字列の先頭と末尾の空白はパースに影響しませんが、空白を入れた場合 証明状態 やエラーメッセージで構文を表示する時に Lean が対応する位置に空白が挿入されます。通常、構文規則のアトムとして出現する有効な識別子は予約キーワードになります。文字列リテラルの前にアンパサンド（&）を置くとこの動作が抑制されます：

stx ::= ...
    | &str

識別子は、指定された位置で期待される構文カテゴリを指定し、オプションで優先順位を指定できます：

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

修飾子 * はクリーネスターで、直前の構文の0回以上の繰り返しにマッチします。これは 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 *

修飾子 + は直前の構文の1回以上の繰り返しにマッチします。これは 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 +

修飾性 ? は部分項をオプショナルにし、直前の構文の繰り返しに0回または1回（それ以上は繰り返さない）にマッチします。これは 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 ::= ...
    | Returns `some x` if `f` succeeds with value `x`, else returns `none`.
optional(stx)

修飾子 ,* はカンマで区切られた直前の構文の0回以上の繰り返しにマッチします。これは 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 ,*

修飾子 ,+ はカンマで区切られた直前の構文の1回以上の繰り返しにマッチします。これは 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 ,+

修飾子 ,*,? はカンマで区切られた直前の構文の0回以上の繰り返しにマッチし、繰り返しの最後のカンマを任意にすることができます。これは allowTrailingSep を伴った sepBy と書くこともできます。

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

修飾子 ,+,? はカンマで区切られた直前の構文の1回以上の繰り返しにマッチし、繰り返しの最後のカンマを任意にすることができます。これは allowTrailingSep を伴った sepBy1 と書くこともできます。

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 を使って定義することができます。後者は繰り返される構文のインスタンスが少なくとも1つ必要です。

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

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

区切り文字を使った繰り返しは sepBy と sepBy1 を使って定義することができ、それぞれ0個以上・1個以上の出現にマッチし、他の構文で区切られます。使い方は3種類あります：

• パラメータが2つの場合は、文字列リテラルで指定されたアトムを使用して区切り文字をパースし、末尾の区切り文字を許容しません。

• パラメータが3つの場合は、3番目のパラメータを使用して区切り文字をパースし、プリティプリンタのためにアトムを使用します。

• パラメータが4つの場合、オプションとしてシーケンスの最後にセパレータを追加することができます。第4引数は常にキーワード 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.