Loading the analysis result of a module.

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

This is copied from DocGen4.envOfImports.

Equations

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

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

This is copied from DocGen4.load.

Equations

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

def BlueprintGen.latexOfImportModule (module : Lean.Name) : IO Latex

Outputs the blueprint of a module.

Equations

• BlueprintGen.latexOfImportModule module = BlueprintGen.runEnvOfImports #[module] (BlueprintGen.moduleToLatexHeader module)

def BlueprintGen.jsonOfImportModule (module : Lean.Name) : IO Lean.Json

Outputs the JSON data for the blueprint of a module.

Equations

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