We define the blueprint_comment /-- ... -/ command that adds a piece of text to the blueprint.

opaque Architect.moduleBlueprintDocExt : Lean.SimplePersistentEnvExtension Lean.ModuleDoc (Lean.PersistentArray Lean.ModuleDoc)

def Architect.addMainModuleBlueprintDoc (env : Lean.Environment) (doc : Lean.ModuleDoc) : Lean.Environment

Equations

• Architect.addMainModuleBlueprintDoc env doc = Lean.PersistentEnvExtension.addEntry Architect.moduleBlueprintDocExt env doc

def Architect.getMainModuleBlueprintDoc (env : Lean.Environment) : Lean.PersistentArray Lean.ModuleDoc

Equations

• Architect.getMainModuleBlueprintDoc env = Architect.moduleBlueprintDocExt.getState env

def Architect.getModuleBlueprintDoc? (env : Lean.Environment) (moduleName : Lean.Name) : Option (Array Lean.ModuleDoc)

Equations

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

def Architect.blueprintComment : Lean.ParserDescr

blueprint_comment /-- ... -/ adds a piece of text to the blueprint of the current module, which is available as \inputleanmodule{Module} in LaTeX.

Equations

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