Environment extension for declaration ranges

opaque Lean.builtinDeclRanges : IO.Ref (Lean.NameMap Lean.DeclarationRanges)

opaque Lean.declRangeExt : Lean.MapDeclarationExtension Lean.DeclarationRanges

def Lean.addBuiltinDeclarationRanges (declName : Lean.Name) (declRanges : Lean.DeclarationRanges) : IO Unit

Equations

• Lean.addBuiltinDeclarationRanges declName declRanges = ST.Ref.modify Lean.builtinDeclRanges fun (x : Lean.NameMap Lean.DeclarationRanges) => x.insert declName declRanges

def Lean.addDeclarationRanges {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) (declRanges : Lean.DeclarationRanges) : m Unit

Equations

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

def Lean.findDeclarationRangesCore? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) : m (Option Lean.DeclarationRanges)

Equations

• Lean.findDeclarationRangesCore? declName = do let __do_lift ← Lean.getEnv pure (Lean.declRangeExt.find? __do_lift declName)

def Lean.findDeclarationRanges? {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadLiftT BaseIO m] (declName : Lean.Name) : m (Option Lean.DeclarationRanges)

Equations

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