Loading the analysis result of a module.

def Architect.envOfImports (imports : Array Lean.Name) : IO Lean.Environment

This is copied from DocGen4.envOfImports.

Equations

• Architect.envOfImports imports = do Architect.envOfImports.unsafe_impl_3 Lean.importModules (Array.map (fun (x : Lean.Name) => { module := x }) imports) Lean.Options.empty 0 #[] true true

def Architect.runEnvOfImports {α : Type} (imports : Array Lean.Name) (options : Lean.Options) (x : Lean.CoreM α) : IO α

This is copied from DocGen4.load, except for separate handling of options.

Equations

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

def Architect.latexOutputOfImportModule (module : Lean.Name) (options : Lean.Options) : IO LatexOutput

Outputs the blueprint of a module.

Equations

• Architect.latexOutputOfImportModule module options = Architect.runEnvOfImports #[module] options (Architect.moduleToLatexOutput module)

def Architect.jsonOfImportModule (module : Lean.Name) (options : Lean.Options) : IO Lean.Json

Outputs the JSON data for the blueprint of a module.

Equations

• Architect.jsonOfImportModule module options = Architect.runEnvOfImports #[module] options (Architect.moduleToJson module)