structure String.Range : Type

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.

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

instance String.instInhabitedRange : Inhabited String.Range

Equations

• String.instInhabitedRange = { default := { start := default, stop := default } }

instance String.instReprRange : Repr String.Range

Equations

• String.instReprRange = { reprPrec := String.reprRange✝ }

instance String.instBEqRange : BEq String.Range

Equations

• String.instBEqRange = { beq := String.beqRange✝ }

instance String.instHashableRange : Hashable String.Range

Equations

• String.instHashableRange = { hash := String.hashRange✝ }

def String.Range.contains (r : String.Range) (pos : String.Pos) (includeStop : optParam Bool false) : Bool

Equations

• r.contains pos includeStop = (decide (r.start ≤ pos) && if includeStop = true then decide (pos ≤ r.stop) else decide (pos < r.stop))

def String.Range.includes (super : String.Range) (sub : String.Range) : Bool

Equations

• super.includes sub = (decide (super.start ≤ sub.start) && decide (super.stop ≥ sub.stop))

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

Equations

• Lean.SourceInfo.updateTrailing trailing x = match x with | Lean.SourceInfo.original leading pos trailing_1 endPos => Lean.SourceInfo.original leading pos trailing endPos | info => info

def Lean.SourceInfo.getRange? (canonicalOnly : optParam Bool false) (info : Lean.SourceInfo) : Option String.Range

Equations

• Lean.SourceInfo.getRange? canonicalOnly info = do let __do_lift ← info.getPos? canonicalOnly let __do_lift_1 ← info.getTailPos? canonicalOnly pure { start := __do_lift, stop := __do_lift_1 }

instance Lean.instBEqSourceInfo_lean : BEq Lean.SourceInfo

Equations

• Lean.instBEqSourceInfo_lean = { beq := Lean.beqSourceInfo✝ }

Syntax AST

inductive Lean.IsNode : Lean.Syntax → Prop

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

def Lean.SyntaxNode : Type

Equations

• Lean.SyntaxNode = { s : Lean.Syntax // Lean.IsNode s }

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

Equations

• Lean.unreachIsNodeMissing a = nomatch a

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

Equations

• Lean.unreachIsNodeAtom a = nomatch a

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

Equations

• Lean.unreachIsNodeIdent a = nomatch a

def Lean.isLitKind (k : Lean.SyntaxNodeKind) : Bool

Equations

• Lean.isLitKind k = (k == Lean.strLitKind || k == Lean.numLitKind || k == Lean.charLitKind || k == Lean.nameLitKind || k == Lean.scientificLitKind)

@[inline]

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

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 : Array Lean.Syntax → β) : β

Equations

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

@[inline]

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

Equations

• n.getNumArgs = n.withArgs fun (args : Array Lean.Syntax) => args.size

@[inline]

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

Equations

• n.getArg i = n.withArgs fun (args : Array Lean.Syntax) => args.get! i

@[inline]

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

Equations

• n.getArgs = n.withArgs fun (args : Array Lean.Syntax) => args

@[inline]

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

Equations

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

partial def Lean.Syntax.structRangeEq : Lean.Syntax → Lean.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 : Lean.Options) (stx1 : Lean.Syntax) (stx2 : Lean.Syntax) : Bool

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

Equations

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

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

Full comparison of syntax structures and source infos.

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

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

Equations

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

def Lean.Syntax.getAtomVal : Lean.Syntax → String

Equations

• x.getAtomVal = match x with | Lean.Syntax.atom info val => val | x => ""

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

Equations

• x✝.setAtomVal x = match x✝, x with | Lean.Syntax.atom info val, v => Lean.Syntax.atom info v | stx, x => stx

@[inline]

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

Equations

• stx.ifNode hyes hno = match stx with | Lean.Syntax.node i k args => hyes ⟨Lean.Syntax.node i k args, ⋯⟩ | x => hno ()

@[inline]

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

Equations

• stx.ifNodeKind kind hyes hno = match stx with | Lean.Syntax.node i k args => if (k == kind) = true then hyes ⟨Lean.Syntax.node i k args, ⋯⟩ else hno () | x => hno ()

def Lean.Syntax.asNode : Lean.Syntax → Lean.SyntaxNode

Equations

• x.asNode = match x with | Lean.Syntax.node info kind args => ⟨Lean.Syntax.node info kind args, ⋯⟩ | x => ⟨Lean.mkNullNode, Lean.Syntax.asNode.proof_1⟩

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

Equations

• stx.getIdAt i = (stx.getArg i).getId

partial def Lean.Syntax.hasIdent (id : Lake.Name) : Lean.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 : Lean.Syntax) (fn : Array Lean.Syntax → Array Lean.Syntax) : Lean.Syntax

Equations

• stx.modifyArgs fn = match stx with | Lean.Syntax.node i k args => Lean.Syntax.node i k (fn args) | stx => stx

@[inline]

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

Equations

• stx.modifyArg i fn = match stx with | Lean.Syntax.node info k args => Lean.Syntax.node info k (args.modify i fn) | stx => stx

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

Equations

• Lean.Syntax.rewriteBottomUp fn stx = (Lean.Syntax.rewriteBottomUpM fn stx).run

def Lean.Syntax.updateLeading : Lean.Syntax → Lean.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.

Equations

• stx.updateLeading = StateT.run' (Lean.Syntax.replaceM Lean.Syntax.updateLeadingAux stx) 0

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

def Lean.Syntax.identComponents (stx : Lean.Syntax) (nFields? : optParam (Option Nat) none) : List Lean.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].

Equations

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

def Lean.Syntax.identComponents.nameComps (n : Lake.Name) (nFields? : Option Nat) : List Lake.Name

Equations

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

structure Lean.Syntax.TopDown : Type

• firstChoiceOnly : Bool
• stx : Lean.Syntax

def Lean.Syntax.topDown (stx : Lean.Syntax) (firstChoiceOnly : optParam Bool false) : Lean.Syntax.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.

Equations

• stx.topDown firstChoiceOnly = { firstChoiceOnly := firstChoiceOnly, stx := stx }

instance Lean.Syntax.instForInTopDown {m : Type u_1 → Type u_2} : ForIn m Lean.Syntax.TopDown Lean.Syntax

Equations

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

@[specialize #[]]

partial def Lean.Syntax.instForInTopDown.loop {m : Type u_1 → Type u_2} : {β : Type u_1} → [inst : Monad m] → (Lean.Syntax → β → m (ForInStep β)) → Bool → Lean.Syntax → β → [inst : Inhabited β] → m (ForInStep β)

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

def Lean.Syntax.reprint.reprintLeaf (info : Lean.SourceInfo) (val : String) : String

Equations

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

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

Equations

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

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

Equations

• stx.getRange? canonicalOnly = match stx.getPos? canonicalOnly, stx.getTailPos? canonicalOnly with | some start, some stop => some { start := start, stop := stop } | x, x_1 => none

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

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

Equations

• Lean.Syntax.ofRange range canonical = Lean.Syntax.atom (Lean.SourceInfo.synthetic range.start range.stop canonical) ""

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 : Lean.Syntax
• parents : Array Lean.Syntax
• idxs : Array Nat

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

Equations

• Lean.Syntax.Traverser.fromSyntax stx = { cur := stx, parents := #[], idxs := #[] }

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

Equations

• t.setCur stx = { cur := stx, parents := t.parents, idxs := t.idxs }

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• t.left = if t.parents.size > 0 then t.up.down (t.idxs.back - 1) else t

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

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

Equations

• t.right = if t.parents.size > 0 then t.up.down (t.idxs.back + 1) else t

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

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

• st : MonadState Lean.Syntax.Traverser m

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

Equations

• Lean.Syntax.MonadTraverser.getCur = Lean.Syntax.Traverser.cur <$> get

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

Equations

• Lean.Syntax.MonadTraverser.setCur stx = modify fun (t : Lean.Syntax.Traverser) => t.setCur stx

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

Equations

• Lean.Syntax.MonadTraverser.goDown idx = modify fun (t : Lean.Syntax.Traverser) => t.down idx

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

Equations

• Lean.Syntax.MonadTraverser.goUp = modify fun (t : Lean.Syntax.Traverser) => t.up

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

Equations

• Lean.Syntax.MonadTraverser.goLeft = modify fun (t : Lean.Syntax.Traverser) => t.left

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

Equations

• Lean.Syntax.MonadTraverser.goRight = modify fun (t : Lean.Syntax.Traverser) => t.right

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

Equations

• Lean.Syntax.MonadTraverser.getIdx = do let st ← get pure (st.idxs.back?.getD 0)

@[inline]

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

Equations

• n.getIdAt i = (n.getArg i).getId

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

Equations

• Lean.mkListNode args = Lean.mkNullNode args

def Lean.Syntax.isQuot : Lean.Syntax → Bool

Equations

• x.isQuot = match x with | Lean.Syntax.node info (pre.str "quot") args => true | Lean.Syntax.node info `Lean.Parser.Term.dynamicQuot args => true | x => false

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

Equations

• stx.getQuotContent = let stx := if (stx.getNumArgs == 1) = true then stx[0] else stx; if stx.isOfKind `Lean.Parser.Term.dynamicQuot = true then stx[3] else stx[1]

def Lean.Syntax.isAntiquot : Lean.Syntax → Bool

Equations

• x.isAntiquot = match x with | Lean.Syntax.node info (pre.str "antiquot") args => true | x => false

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

Equations

• stx.isAntiquots = (stx.isAntiquot || stx.isOfKind Lean.choiceKind && decide (stx.getNumArgs > 0) && stx.getArgs.all Lean.Syntax.isAntiquot)

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

Equations

• stx.getCanonicalAntiquot = if stx.isOfKind Lean.choiceKind = true then stx[0] else stx

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

Equations

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

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

Equations

• stx.isEscapedAntiquot = !stx[1].getArgs.isEmpty

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

Equations

• stx.unescapeAntiquot = if stx.isAntiquot = true then stx.setArg 1 (Lean.mkNullNode stx[1].getArgs.pop) else stx

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

Equations

• stx.getAntiquotTerm = let e := if stx.isAntiquot = true then stx[2] else stx[3]; if e.isIdent = true then e else if e.isAtom = true then (Lean.mkNode `Lean.Parser.Term.hole #[e]).raw else e[1]

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

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

Equations

• x.antiquotKind? = match x with | Lean.Syntax.node info ((k.str "pseudo").str "antiquot") args => some (k, true) | Lean.Syntax.node info (k.str "antiquot") args => some (k, false) | x => none

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

Equations

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

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

Equations

• x.antiquotSpliceKind? = match x with | Lean.Syntax.node info (k.str "antiquot_scope") args => some k | x => none

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

Equations

• stx.isAntiquotSplice = stx.antiquotSpliceKind?.isSome

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

Equations

• stx.getAntiquotSpliceContents = stx[3].getArgs

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

Equations

• stx.getAntiquotSpliceSuffix = if stx.isAntiquotSplice = true then stx[5] else stx[1]

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

Equations

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

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

Equations

• x.antiquotSuffixSplice? = match x with | Lean.Syntax.node info (k.str "antiquot_suffix_splice") args => some k | x => none

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

Equations

• stx.isAntiquotSuffixSplice = stx.antiquotSuffixSplice?.isSome

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

Equations

• stx.getAntiquotSuffixSpliceInner = stx[0]

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

Equations

• Lean.Syntax.mkAntiquotSuffixSpliceNode kind inner suffix = (Lean.mkNode (kind ++ `antiquot_suffix_splice) #[inner, Lean.mkAtom suffix]).raw

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

Equations

• stx.isTokenAntiquot = stx.isOfKind `token_antiquot

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

Equations

• stx.isAnyAntiquot = (stx.isAntiquot || stx.isAntiquotSplice || stx.isAntiquotSuffixSplice || stx.isTokenAntiquot)

@[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.

Equations

• Lean.Syntax.Stack = List (Lean.Syntax × Nat)

def Lean.Syntax.findStack? (root : Lean.Syntax) (visit : Lean.Syntax → Bool) (accept : optParam (Lean.Syntax → Bool) fun (stx : Lean.Syntax) => !stx.hasArgs) : Option Lean.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.

Equations

• root.findStack? visit accept = if visit root = true then Lean.Syntax.findStack?.go visit accept [] root else none

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

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

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.