Equations
- One or more equations did not get rendered due to their size.
- mk: ∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax), Lean.IsNode (Lean.Syntax.node info kind args)
Equations
- Lean.unreachIsNodeMissing h = False.elim (_ : False)
def
Lean.unreachIsNodeAtom
{β : Sort u_1}
{info : Lean.SourceInfo}
{val : String}
(h : Lean.IsNode (Lean.Syntax.atom info val))
:
β
Equations
- Lean.unreachIsNodeAtom h = False.elim (_ : False)
def
Lean.unreachIsNodeIdent
{β : Sort u_1}
{info : Lean.SourceInfo}
{rawVal : Substring}
{val : Lean.Name}
{preresolved : List (Lean.Name × List String)}
(h : Lean.IsNode (Lean.Syntax.ident info rawVal val preresolved))
:
β
Equations
- Lean.unreachIsNodeIdent h = False.elim (_ : False)
Equations
@[inline]
Equations
- One or more equations did not get rendered due to their size.
@[inline]
Equations
- One or more equations did not get rendered due to their size.
@[inline]
Equations
- Lean.SyntaxNode.getNumArgs n = Lean.SyntaxNode.withArgs n fun args => Array.size args
@[inline]
Equations
- Lean.SyntaxNode.getArg n i = Lean.SyntaxNode.withArgs n fun args => Array.get! args i
@[inline]
Equations
- Lean.SyntaxNode.getArgs n = Lean.SyntaxNode.withArgs n fun args => args
@[inline]
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
- Lean.Syntax.setAtomVal _fun_discr _fun_discr = match _fun_discr, _fun_discr 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
- 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 : Lean.SyntaxNode → β)
(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
- Lean.Syntax.getIdAt stx i = Lean.Syntax.getId (Lean.Syntax.getArg stx i)
@[inline]
Equations
- Lean.Syntax.modifyArgs stx fn = match stx with | Lean.Syntax.node i k args => Lean.Syntax.node i k (fn args) | stx => stx
@[inline]
Equations
- Lean.Syntax.modifyArg stx i fn = match stx with | Lean.Syntax.node info k args => Lean.Syntax.node info k (Array.modify args i fn) | stx => stx
@[specialize]
partial def
Lean.Syntax.replaceM
{m : Type → Type}
[inst : Monad m]
(fn : Lean.Syntax → m (Option Lean.Syntax))
:
@[specialize]
partial def
Lean.Syntax.rewriteBottomUpM
{m : Type → Type}
[inst : Monad m]
(fn : Lean.Syntax → m Lean.Syntax)
:
@[inline]
Equations
- Lean.Syntax.rewriteBottomUp fn stx = Id.run (Lean.Syntax.rewriteBottomUpM fn stx)
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
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.
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
- Lean.Syntax.topDown stx firstChoiceOnly = { firstChoiceOnly := firstChoiceOnly, stx := stx }
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 : Monad m] →
(Lean.Syntax → β → m (ForInStep β)) → Bool → Lean.Syntax → β → [inst : Inhabited β] → m (ForInStep β)
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.
- cur : Lean.Syntax
- parents : Array Lean.Syntax
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.
Equations
- Lean.Syntax.Traverser.fromSyntax stx = { cur := stx, parents := #[], idxs := #[] }
Equations
- Lean.Syntax.Traverser.setCur t stx = { 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
- Lean.Syntax.Traverser.left t = if Array.size t.parents > 0 then Lean.Syntax.Traverser.down (Lean.Syntax.Traverser.up t) (Array.back t.idxs - 1) else t
Advance to the right sibling of the current node, if any.
Equations
- Lean.Syntax.Traverser.right t = if Array.size t.parents > 0 then Lean.Syntax.Traverser.down (Lean.Syntax.Traverser.up t) (Array.back t.idxs + 1) else t
- st : MonadState Lean.Syntax.Traverser m
Monad class that gives read/write access to a Traverser.
def
Lean.Syntax.MonadTraverser.getCur
{m : Type → Type}
[inst : Monad m]
[t : Lean.Syntax.MonadTraverser m]
:
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.setCur t 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.down t idx
Equations
- Lean.Syntax.MonadTraverser.goUp = modify fun t => Lean.Syntax.Traverser.up t
Equations
- Lean.Syntax.MonadTraverser.goLeft = modify fun t => Lean.Syntax.Traverser.left t
Equations
- Lean.Syntax.MonadTraverser.goRight = modify fun t => Lean.Syntax.Traverser.right t
def
Lean.Syntax.MonadTraverser.getIdx
{m : Type → Type}
[inst : Monad m]
[t : Lean.Syntax.MonadTraverser m]
:
m Nat
Equations
- Lean.Syntax.MonadTraverser.getIdx = do let st ← get pure (Option.getD (Array.back? st.idxs) 0)
@[inline]
Equations
Equations
- Lean.mkListNode args = Lean.mkNullNode args
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
- Lean.Syntax.isAntiquot _fun_discr = match _fun_discr with | Lean.Syntax.node info (Lean.Name.str a "antiquot" a_1) args => true | x => false
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Syntax.getCanonicalAntiquot stx = if Lean.Syntax.isOfKind stx Lean.choiceKind = true then Lean.Syntax.getOp stx 0 else stx
Equations
Equations
- Lean.Syntax.unescapeAntiquot stx = if Lean.Syntax.isAntiquot stx = true then Lean.Syntax.setArg stx 1 (Lean.mkNullNode (Array.pop (Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1)))) else stx
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
- Lean.Syntax.antiquotSpliceKind? _fun_discr = match _fun_discr with | Lean.Syntax.node info (Lean.Name.str k "antiquot_scope" a) args => some k | x => none
Equations
Equations
Equations
- Lean.Syntax.getAntiquotSpliceSuffix stx = if Lean.Syntax.isAntiquotSplice stx = true then Lean.Syntax.getOp stx 5 else Lean.Syntax.getOp stx 1
def
Lean.Syntax.mkAntiquotSpliceNode
(kind : Lean.SyntaxNodeKind)
(contents : Array Lean.Syntax)
(suffix : String)
(nesting : optParam Nat 0)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Syntax.antiquotSuffixSplice? _fun_discr = match _fun_discr with | Lean.Syntax.node info (Lean.Name.str k "antiquot_suffix_splice" a) args => some k | x => none
Equations
Equations
def
Lean.Syntax.mkAntiquotSuffixSpliceNode
(kind : Lean.SyntaxNodeKind)
(inner : Lean.Syntax)
(suffix : String)
:
Equations
- Lean.Syntax.mkAntiquotSuffixSpliceNode kind inner suffix = (Lean.mkNode (kind ++ `antiquot_suffix_splice) #[inner, Lean.mkAtom suffix]).raw
Equations
- Lean.Syntax.isTokenAntiquot stx = Lean.Syntax.isOfKind stx `token_antiquot