Documentation

Lean.Elab.DeclarationRange

def Lean.Elab.getDeclarationRange {m : TypeType} [inst : Monad m] [inst : Lean.MonadFileMap m] (stx : Lean.Syntax) :
Equations
def Lean.Elab.addDeclarationRanges {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadFileMap m] (declName : Lean.Name) (stx : Lean.Syntax) :
Equations
def Lean.Elab.addAuxDeclarationRanges {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadFileMap m] (declName : Lean.Name) (stx : Lean.Syntax) (header : Lean.Syntax) :
Equations