structure Lean.Syntax.Range : Type

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

• start : String.Pos.Raw
• stop : String.Pos.Raw

@[implicit_reducible]

instance Lean.Syntax.instInhabitedRange : Inhabited Syntax.Range

def Lean.Syntax.instInhabitedRange.default : Syntax.Range

@[implicit_reducible]

instance Lean.Syntax.instReprRange : Repr Syntax.Range

def Lean.Syntax.instReprRange.repr : Syntax.Range → Nat → Format

@[implicit_reducible]

instance Lean.Syntax.instBEqRange : BEq Syntax.Range

def Lean.Syntax.instBEqRange.beq : Syntax.Range → Syntax.Range → Bool

def Lean.Syntax.instHashableRange.hash : Syntax.Range → UInt64

@[implicit_reducible]

instance Lean.Syntax.instHashableRange : Hashable Syntax.Range

@[deprecated Lean.Syntax.Range (since := "2025-10-20")]

def String.Range : Type

def Lean.Syntax.Range.contains (r : Syntax.Range) (pos : String.Pos.Raw) (includeStop : Bool := false) : Bool

def Lean.Syntax.Range.includes (super sub : Syntax.Range) (includeSuperStop includeSubStop : Bool := false) : Bool

Checks whether sub is contained in super. includeSuperStop and includeSubStop control whether super and sub have an inclusive upper bound.

@[deprecated Lean.Syntax.Range.includes (since := "2025-10-20")]

def String.Range.includes (super sub : Lean.Syntax.Range) (includeSuperStop includeSubStop : Bool := false) : Bool

def Lean.Syntax.Range.overlaps (first second : Syntax.Range) (includeFirstStop includeSecondStop : Bool := false) : Bool

@[deprecated Lean.Syntax.Range.overlaps (since := "2025-10-20")]

def String.Range.overlaps (first second : Lean.Syntax.Range) (includeFirstStop includeSecondStop : Bool := false) : Bool

def Lean.Syntax.Range.bsize (r : Syntax.Range) : Nat

@[deprecated Lean.Syntax.Range.bsize (since := "2025-10-20")]

def String.Range.bsize (r : Lean.Syntax.Range) : Nat

def Lean.SourceInfo.updateTrailing (trailing : Substring.Raw) : SourceInfo → SourceInfo

def Lean.SourceInfo.getRange? (canonicalOnly : Bool := false) (info : SourceInfo) : Option Syntax.Range

def Lean.SourceInfo.getRangeWithTrailing? (canonicalOnly : Bool := false) (info : SourceInfo) : Option Syntax.Range

def Lean.SourceInfo.nonCanonicalSynthetic : SourceInfo → SourceInfo

Converts an original or synthetic (canonical := true) SourceInfo to a synthetic (canonical := false) SourceInfo. This is sometimes useful when SourceInfo is being moved around between Syntaxes.

def Lean.instBEqSourceInfo_lean.beq : SourceInfo → SourceInfo → Bool

@[implicit_reducible]

instance Lean.instBEqSourceInfo_lean : BEq SourceInfo

Syntax AST

inductive Lean.IsNode : Syntax → Prop

• mk (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node info kind args)

def Lean.SyntaxNode : Type

def Lean.unreachIsNodeMissing {β : Sort u_1} : IsNode Syntax.missing → β

def Lean.unreachIsNodeAtom {β : Sort u_1} {info : SourceInfo} {val : String} : IsNode (Syntax.atom info val) → β

def Lean.unreachIsNodeIdent {β : Sort u_1} {info : SourceInfo} {rawVal : Substring.Raw} {val : Name} {preresolved : List Syntax.Preresolved} : IsNode (Syntax.ident info rawVal val preresolved) → β

def Lean.isLitKind (k : SyntaxNodeKind) : Bool

@[inline]

def Lean.SyntaxNode.getKind (n : SyntaxNode) : SyntaxNodeKind

@[inline]

def Lean.SyntaxNode.withArgs {β : Sort u_1} (n : SyntaxNode) (fn : Array Syntax → β) : β

@[inline]

def Lean.SyntaxNode.getNumArgs (n : SyntaxNode) : Nat

@[inline]

def Lean.SyntaxNode.getArg (n : SyntaxNode) (i : Nat) : Syntax

@[inline]

def Lean.SyntaxNode.getArgs (n : SyntaxNode) : Array Syntax

@[inline]

def Lean.SyntaxNode.modifyArgs (n : SyntaxNode) (fn : Array Syntax → Array Syntax) : Syntax

partial def Lean.Syntax.structRangeEq : Syntax → Syntax → Bool

Compares syntax structures and position ranges, but not whitespace. We generally assume that if syntax trees equal in this way generate the same elaboration output, including positions contained in e.g. diagnostics and the info tree. However, as we have a few request handlers such as goalsAt? that are sensitive to whitespace information in the info tree, we currently use eqWithInfo instead for reuse checks.

def Lean.Syntax.structRangeEqWithTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool

Like structRangeEq but prints trace on failure if trace.Elab.reuse is activated.

partial def Lean.Syntax.eqWithInfo : Syntax → Syntax → Bool

Full comparison of syntax structures and source infos.

def Lean.Syntax.eqWithInfoAndTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool

Like eqWithInfo but prints trace on failure if trace.Elab.reuse is activated.

def Lean.Syntax.getAtomVal : Syntax → String

def Lean.Syntax.setAtomVal : Syntax → String → Syntax

@[inline]

def Lean.Syntax.ifNode {β : Sort u_1} (stx : Syntax) (hyes : SyntaxNode → β) (hno : Unit → β) : β

@[inline]

def Lean.Syntax.ifNodeKind {β : Sort u_1} (stx : Syntax) (kind : SyntaxNodeKind) (hyes : SyntaxNode → β) (hno : Unit → β) : β

def Lean.Syntax.asNode : Syntax → SyntaxNode

def Lean.Syntax.getIdAt (stx : Syntax) (i : Nat) : Name

partial def Lean.Syntax.hasIdent (id : Name) : Syntax → Bool

Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

@[inline]

def Lean.Syntax.modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) : Syntax

@[inline]

def Lean.Syntax.modifyArg (stx : Syntax) (i : Nat) (fn : Syntax → Syntax) : Syntax

@[specialize #[]]

partial def Lean.Syntax.replaceM {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m Syntax

@[specialize #[]]

partial def Lean.Syntax.rewriteBottomUpM {m : Type → Type} [Monad m] (fn : Syntax → m Syntax) : Syntax → m Syntax

@[inline]

def Lean.Syntax.rewriteBottomUp (fn : Syntax → Syntax) (stx : Syntax) : Syntax

def Lean.Syntax.updateLeading : Syntax → Syntax

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.

partial def Lean.Syntax.updateTrailing (trailing : Substring.Raw) : Syntax → Syntax

def Lean.Syntax.identComponents (stx : Syntax) (nFields? : Option Nat := none) : List Syntax

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].

structure Lean.Syntax.TopDown : Type

• firstChoiceOnly : Bool
• stx : Syntax

def Lean.Syntax.topDown (stx : Syntax) (firstChoiceOnly : Bool := false) : TopDown

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.

@[implicit_reducible]

instance Lean.Syntax.instForInTopDownOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m TopDown Syntax

@[specialize #[]]

partial def Lean.Syntax.instForInTopDownOfMonad.loop {m : Type u_1 → Type u_2} [Monad m] {β✝ : Type u_1} (f : Syntax → β✝ → m (ForInStep β✝)) (firstChoiceOnly : Bool) (stx : Syntax) (b : β✝) [Inhabited β✝] : m (ForInStep β✝)

partial def Lean.Syntax.reprint (stx : Syntax) : Option String

def Lean.Syntax.hasMissing (stx : Syntax) : Bool

def Lean.Syntax.getRange? (stx : Syntax) (canonicalOnly : Bool := false) : Option Syntax.Range

def Lean.Syntax.getRangeWithTrailing? (stx : Syntax) (canonicalOnly : Bool := false) : Option Syntax.Range

def Lean.Syntax.ofRange (range : Syntax.Range) (canonical : Bool := true) : Syntax

Returns a synthetic Syntax which has the specified Lean.Syntax.Range.

structure Lean.Syntax.Traverser : Type

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.

• cur : Syntax
• parents : Array Syntax
• idxs : Array Nat

def Lean.Syntax.Traverser.fromSyntax (stx : Syntax) : Traverser

def Lean.Syntax.Traverser.setCur (t : Traverser) (stx : Syntax) : Traverser

def Lean.Syntax.Traverser.down (t : Traverser) (idx : Nat) : Traverser

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

def Lean.Syntax.Traverser.up (t : Traverser) : Traverser

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

def Lean.Syntax.Traverser.left (t : Traverser) : Traverser

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

def Lean.Syntax.Traverser.right (t : Traverser) : Traverser

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

class Lean.Syntax.MonadTraverser (m : Type → Type) : Type 1

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

• st : MonadState Traverser m

def Lean.Syntax.MonadTraverser.getCur {m : Type → Type} [Monad m] [t : MonadTraverser m] : m Syntax

def Lean.Syntax.MonadTraverser.setCur {m : Type → Type} [t : MonadTraverser m] (stx : Syntax) : m Unit

def Lean.Syntax.MonadTraverser.goDown {m : Type → Type} [t : MonadTraverser m] (idx : Nat) : m Unit

def Lean.Syntax.MonadTraverser.goUp {m : Type → Type} [t : MonadTraverser m] : m Unit

def Lean.Syntax.MonadTraverser.goLeft {m : Type → Type} [t : MonadTraverser m] : m Unit

def Lean.Syntax.MonadTraverser.goRight {m : Type → Type} [t : MonadTraverser m] : m Unit

def Lean.Syntax.MonadTraverser.getIdx {m : Type → Type} [Monad m] [t : MonadTraverser m] : m Nat

@[inline]

def Lean.SyntaxNode.getIdAt (n : SyntaxNode) (i : Nat) : Name

def Lean.mkListNode (args : Array Syntax) : Syntax

def Lean.Syntax.isQuot : Syntax → Bool

def Lean.Syntax.getQuotContent (stx : Syntax) : Syntax

def Lean.Syntax.isAntiquot : Syntax → Bool

def Lean.Syntax.isAntiquots (stx : Syntax) : Bool

def Lean.Syntax.getCanonicalAntiquot (stx : Syntax) : Syntax

def Lean.Syntax.mkAntiquotNode (kind : Name) (term : Syntax) (nesting : Nat := 0) (name : Option String := none) (isPseudoKind : Bool := false) : Syntax

def Lean.Syntax.isEscapedAntiquot (stx : Syntax) : Bool

def Lean.Syntax.unescapeAntiquot (stx : Syntax) : Syntax

def Lean.Syntax.getAntiquotTerm (stx : Syntax) : Syntax

def Lean.Syntax.antiquotKind? : Syntax → Option (SyntaxNodeKind × Bool)

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

def Lean.Syntax.antiquotKinds (stx : Syntax) : List (SyntaxNodeKind × Bool)

def Lean.Syntax.antiquotSpliceKind? : Syntax → Option SyntaxNodeKind

def Lean.Syntax.isAntiquotSplice (stx : Syntax) : Bool

def Lean.Syntax.getAntiquotSpliceContents (stx : Syntax) : Array Syntax

def Lean.Syntax.getAntiquotSpliceSuffix (stx : Syntax) : Syntax

def Lean.Syntax.mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting : Nat := 0) : Syntax

def Lean.Syntax.antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind

def Lean.Syntax.isAntiquotSuffixSplice (stx : Syntax) : Bool

def Lean.Syntax.getAntiquotSuffixSpliceInner (stx : Syntax) : Syntax

def Lean.Syntax.mkAntiquotSuffixSpliceNode (kind : SyntaxNodeKind) (inner : Syntax) (suffix : String) : Syntax

def Lean.Syntax.isTokenAntiquot (stx : Syntax) : Bool

def Lean.Syntax.isAnyAntiquot (stx : Syntax) : Bool

@[reducible, inline]

abbrev Lean.Syntax.Stack : Type

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.

def Lean.Syntax.findStack? (root : Syntax) (visit : Syntax → Bool) (accept : Syntax → Bool := fun (stx : Syntax) => !stx.hasArgs) : Option Syntax.Stack

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

def Lean.Syntax.Stack.matches (stack : Syntax.Stack) (pattern : List (Option SyntaxNodeKind)) : Bool

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