Equations
Instances For
Checks whether sub
is contained in super
.
includeSuperStop
and includeSubStop
control whether super
and sub
have
an inclusive upper bound.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
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 Syntax
es.
Equations
Instances For
Syntax AST #
- mk (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node info kind args)
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
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.
Like structRangeEq
but prints trace on failure if trace.Elab.reuse
is activated.
Equations
Instances For
Full comparison of syntax structures and source infos.
Equations
Instances For
Equations
Instances For
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.
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
Instances For
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
Instances For
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
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Advance to the idx
-th child of the current node.
Equations
Instances For
Advance to the parent of the current node, if any.
Equations
Instances For
Advance to the left sibling of the current node, if any.
Equations
Instances For
Advance to the right sibling of the current node, if any.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see mkAntiquot
).
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
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
Instances For
Compare the SyntaxNodeKind
s in pattern
to those of the Syntax
elements in stack
. Return false
if stack
is shorter than pattern
.