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

Lean.findDocString? env declName = do let a ← ST.Ref.get Lean.builtinDocStrings pure (Option.orElse (Lean.NameMap.find? a declName) fun x => Lean.MapDeclarationExtension.find? Lean.docStringExt env declName)

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

Lean.Environment

Equations

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

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

Std.PersistentArray String

Equations

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

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

Option (Array String)

Equations

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