def Lean.removeLeadingSpaces (s : String) : String

Equations

• Lean.removeLeadingSpaces s = let n := Lean.findLeadingSpacesSize s; if (n == 0) = true then s else Lean.removeNumLeadingSpaces n s

def Lean.addBuiltinDocString (declName : Lake.Name) (docString : String) : IO Unit

Equations

• Lean.addBuiltinDocString declName docString = ST.Ref.modify Lean.builtinDocStrings fun x => Lean.NameMap.insert x declName (Lean.removeLeadingSpaces docString)

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

Equations

• Lean.addDocString declName docString = Lean.modifyEnv fun env => Lean.MapDeclarationExtension.insert Lean.docStringExt env declName (Lean.removeLeadingSpaces docString)

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

Equations

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

def Lean.findDocString? (env : Lean.Environment) (declName : Lake.Name) (includeBuiltin : optParam Bool true) : 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) : Lean.PersistentArray Lean.ModuleDoc

Equations

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

def Lean.getModuleDoc? (env : Lean.Environment) (moduleName : Lake.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)

def Lean.getDocStringText {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadRef m] (stx : Lean.TSyntax `Lean.Parser.Command.docComment) : m String

Equations

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

def Lean.TSyntax.getDocString (stx : Lean.TSyntax `Lean.Parser.Command.docComment) : String

Equations

• Lean.TSyntax.getDocString stx = match stx.raw[1] with | Lean.Syntax.atom info val => String.extract val 0 (String.endPos val - { byteIdx := 2 }) | x => ""