# Documentation

Lean.Syntax

structure String.Range :

A position range inside a string. This type is mostly in combination with syntax trees, as there might not be a single underlying string in this case that could be used for a Substring.

Instances For
Equations
def String.Range.contains (r : String.Range) (pos : String.Pos) (includeStop : ) :
Equations
Equations
Equations

# Syntax AST #

inductive Lean.IsNode :
Instances For
Equations
def Lean.unreachIsNodeMissing {β : Sort u_1} :
β
Equations
def Lean.unreachIsNodeAtom {β : Sort u_1} {info : Lean.SourceInfo} {val : String} (h : Lean.IsNode (Lean.Syntax.atom info val)) :
β
Equations
def Lean.unreachIsNodeIdent {β : Sort u_1} {info : Lean.SourceInfo} {rawVal : Substring} {val : Lean.Name} {preresolved : } (h : Lean.IsNode (Lean.Syntax.ident info rawVal val preresolved)) :
β
Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.SyntaxNode.withArgs {β : Sort u_1} (n : Lean.SyntaxNode) (fn : ) :
β
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
@[inline]
def Lean.Syntax.ifNode {β : Sort u_1} (stx : Lean.Syntax) (hyes : ) (hno : Unitβ) :
β
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Syntax.ifNodeKind {β : Sort u_1} (stx : Lean.Syntax) (kind : Lean.SyntaxNodeKind) (hyes : ) (hno : Unitβ) :
β
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
@[inline]
Equations
@[inline]
Equations
@[specialize #[]]
partial def Lean.Syntax.replaceM {m : } [inst : ] (fn : ) :
@[specialize #[]]
partial def Lean.Syntax.rewriteBottomUpM {m : } [inst : ] (fn : ) :
@[inline]
Equations

Set SourceInfo.leading according to the trailing stop of the preceding token. The result is a round-tripping syntax tree IF, in the input syntax tree,

• all leading stops, atom contents, and trailing starts are correct
• trailing stops are between the trailing start and the next leading stop.

Remark: after parsing, all SourceInfo.leading fields are empty. The Syntax argument is the output produced by the parser for source. This function "fixes" the source.leading field.

Additionally, we try to choose "nicer" splits between leading and trailing stops according to some heuristics so that e.g. comments are associated to the (intuitively) correct token.

Note that the SourceInfo.trailing fields must be correct. The implementation of this Function relies on this property.

Equations
partial def Lean.Syntax.updateTrailing (trailing : Substring) :
def Lean.Syntax.identComponents (stx : Lean.Syntax) (nFields? : optParam () none) :

Split an ident into its dot-separated components while preserving source info. Macro scopes are first erased. For example, foo.bla.boo._@._hyg.4[foo, bla, boo]. If nFields is set, we take that many fields from the end and keep the remaining components as one name. For example, foo.bla.boo with (nFields := 1)[foo.bla, boo].

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Syntax.topDown (stx : Lean.Syntax) (firstChoiceOnly : ) :

for _ in stx.topDown iterates through each node and leaf in stx top-down, left-to-right. If firstChoiceOnly is true, only visit the first argument of each choice node.

Equations
instance Lean.Syntax.instForInTopDownSyntax {m : Type u_1 → Type u_2} :
Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
partial def Lean.Syntax.instForInTopDownSyntax.loop {m : Type u_1 → Type u_2} :
{β : Type u_1} → [inst : ] → (Lean.Syntaxβm ()) → BoolLean.Syntaxβ[inst : ] → m ()
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Syntax.getRange? (stx : Lean.Syntax) (canonicalOnly : ) :
Equations
• One or more equations did not get rendered due to their size.

Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right. Indices are allowed to be out-of-bound, in which case cur is Syntax.missing. If the Traverser is used linearly, updates are linear in the Syntax object as well.

Instances For
Equations
• = { cur := stx, parents := #[], idxs := #[] }
Equations
• = { cur := stx, parents := t.parents, idxs := t.idxs }

Advance to the idx-th child of the current node.

Equations
• One or more equations did not get rendered due to their size.

Advance to the parent of the current node, if any.

Equations
• One or more equations did not get rendered due to their size.

Advance to the left sibling of the current node, if any.

Equations

Advance to the right sibling of the current node, if any.

Equations

Monad class that gives read/write access to a Traverser.

Instances
def Lean.Syntax.MonadTraverser.getCur {m : } [inst : ] [t : ] :
Equations
Equations
def Lean.Syntax.MonadTraverser.goDown {m : } [t : ] (idx : Nat) :
Equations
Equations
• Lean.Syntax.MonadTraverser.goUp = modify fun t =>
Equations
• Lean.Syntax.MonadTraverser.goLeft = modify fun t =>
Equations
• Lean.Syntax.MonadTraverser.goRight = modify fun t =>
def Lean.Syntax.MonadTraverser.getIdx {m : } [inst : ] [t : ] :
m Nat
Equations
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = if then stx[0] else stx
def Lean.Syntax.mkAntiquotNode (kind : Lean.Name) (term : Lean.Syntax) (nesting : ) (name : optParam () none) (isPseudoKind : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.

Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see mkAntiquot).

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• = if then stx[5] else stx[1]
def Lean.Syntax.mkAntiquotSpliceNode (kind : Lean.SyntaxNodeKind) (contents : ) (suffix : String) (nesting : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
@[inline]

List of Syntax nodes in which each succeeding element is the parent of the current. The associated index is the index of the preceding element in the list of children of the current element.

Equations
def Lean.Syntax.findStack? (root : Lean.Syntax) (visit : ) (accept : optParam () fun stx => ) :

Return stack of syntax nodes satisfying visit, starting with such a node that also fulfills accept (default "is leaf"), and ending with the root.

Equations
partial def Lean.Syntax.findStack?.go (visit : ) (accept : optParam () fun stx => ) (stack : Lean.Syntax.Stack) (stx : Lean.Syntax) :

Compare the SyntaxNodeKinds in pattern to those of the Syntax elements in stack. Return false if stack is shorter than pattern`.

Equations
• One or more equations did not get rendered due to their size.