Documentation

Lean.DeclarationRange

Environment extension for declaration ranges #

source
opaque Lean.builtinDeclRanges :
IO.Ref (NameMap DeclarationRanges)
source
opaque Lean.declRangeExt :
MapDeclarationExtension DeclarationRanges
source
def Lean.addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) :
IO Unit
Instances For
    source
    def Lean.addDeclarationRanges {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) :
    m Unit
    Instances For
      source
      def Lean.findDeclarationRangesCore? {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) :
      m (Option DeclarationRanges)
      Instances For
        source
        def Lean.findDeclarationRanges? {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) :
        m (Option DeclarationRanges)
        Instances For