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
Equations
    Instances For
      source
      def Lean.addDeclarationRanges {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) :
      m Unit
      Equations
        Instances For
          source
          def Lean.findDeclarationRangesCore? {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) :
          m (Option DeclarationRanges)
          Equations
            Instances For
              source
              def Lean.findDeclarationRanges? {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) :
              m (Option DeclarationRanges)
              Equations
                Instances For