Documentation

Lean.DocString

def Lean.addBuiltinDocString (declName : Lean.Name) (docString : String) :

Equations

Lean.addBuiltinDocString declName docString = ST.Ref.modify Lean.builtinDocStrings fun a => Lean.NameMap.insert a declName docString

def Lean.addDocString {m : Type → Type} [inst : Lean.MonadEnv m] (declName : Lean.Name) (docString : String) :

Equations

Lean.addDocString declName docString = Lean.modifyEnv fun env => Lean.MapDeclarationExtension.insert Lean.docStringExt env declName docString

def Lean.addDocString' {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) (docString? : Option String) :

Equations

Lean.addDocString' declName docString? = match docString? with | some docString => Lean.addDocString declName docString | none => pure ()

def Lean.findDocString? (env : Lean.Environment) (declName : Lean.Name) :

IO (Option String)

Equations

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

structure Lean.ModuleDoc:

Type

doc : String
declarationRange : Lean.DeclarationRange

def Lean.addMainModuleDoc (env : Lean.Environment) (doc : Lean.ModuleDoc) :

Lean.Environment

Equations

Lean.addMainModuleDoc env doc = Lean.PersistentEnvExtension.addEntry Lean.moduleDocExt env doc

def Lean.getMainModuleDoc (env : Lean.Environment) :

Std.PersistentArray Lean.ModuleDoc

Equations

Lean.getMainModuleDoc env = Lean.SimplePersistentEnvExtension.getState Lean.moduleDocExt env

def Lean.getModuleDoc? (env : Lean.Environment) (moduleName : Lean.Name) :

Option (Array Lean.ModuleDoc)

Equations

Lean.getModuleDoc? env moduleName = Option.map (fun modIdx => Lean.PersistentEnvExtension.getModuleEntries Lean.moduleDocExt env modIdx) (Lean.Environment.getModuleIdx? env moduleName)