Documentation

Lean.Elab.DeclarationRange

source
def Lean.Elab.getDeclarationRange {m : Type → Type} [inst : Monad m] [inst : Lean.MonadFileMap m] (stx : Lean.Syntax) :
m Lean.DeclarationRange
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.getDeclarationSelectionRef (stx : Lean.Syntax) :
Lean.Syntax

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.
source
def Lean.Elab.addDeclarationRanges {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadFileMap m] (declName : Lean.Name) (stx : Lean.Syntax) :
m Unit

Store the range and selectionRange for declName where stx is the whole syntax object decribing declName. This method is for the builtin declarations only. User-defined commands should use Lean.addDeclarationRanges to store this information for their commands.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.addAuxDeclarationRanges {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadFileMap m] (declName : Lean.Name) (stx : Lean.Syntax) (header : Lean.Syntax) :
m Unit

Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc.

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