Environment extension for declaration ranges

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

opaque Lean.declRangeExt : MapDeclarationExtension DeclarationRanges

def Lean.addBuiltinDeclarationRanges (declName : Name) (declRanges : 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] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit

Equations

• Lean.addDeclarationRanges declName declRanges = Lean.modifyEnv fun (env : Lean.Environment) => Lean.declRangeExt.insert env declName declRanges

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

Equations

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

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

Equations

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