Equations
- One or more equations did not get rendered due to their size.
Instances For
For most builtin declarations, the selection range is just its name, which is stored in the second position. Example:
"def " >> declId >> optDeclSig >> declVal
If the declaration name is absent, we use the keyword instead.
This function converts the given Syntax
into one that represents its "selection range".
Equations
- One or more equations did not get rendered due to their size.
Instances For
Derives and adds declaration ranges from given syntax trees. If rangeStx
does not have a range,
nothing is added. If selectionRangeStx
does not have a range, it is defaulted to that of
rangeStx
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stores the range
and selectionRange
for declName
where modsStx
is the modifier part and
cmdStx
the remaining part of the syntax tree for declName
.
This method is for the builtin declarations only. User-defined commands should use
Lean.Elab.addDeclarationRangesFromSyntax
or Lean.addDeclarationRanges
to store this information
for their commands.
Equations
- One or more equations did not get rendered due to their size.