The blueprint content in a module (see BlueprintContent) consists of:

• Blueprint nodes generated from @[blueprint] tags
• All module docstrings defined in /-! ... -/

These contents are sorted by declaration range (similar to the sort in doc-gen4).

def BlueprintGen.instReprModuleDoc_blueprintGen.repr : Lean.ModuleDoc → Nat → Std.Format

Equations

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

instance BlueprintGen.instReprModuleDoc_blueprintGen : Repr Lean.ModuleDoc

Equations

• BlueprintGen.instReprModuleDoc_blueprintGen = { reprPrec := BlueprintGen.instReprModuleDoc_blueprintGen.repr }

inductive BlueprintGen.BlueprintContent : Type

The export blueprint LaTeX from a module is determined by the list of BlueprintContent in the module. This is analogous to doc-gen4's ModuleMember.

• node : NodeWithPos → BlueprintContent
• modDoc : Lean.ModuleDoc → BlueprintContent

instance BlueprintGen.instInhabitedBlueprintContent : Inhabited BlueprintContent

Equations

• BlueprintGen.instInhabitedBlueprintContent = { default := BlueprintGen.instInhabitedBlueprintContent.default }

def BlueprintGen.instInhabitedBlueprintContent.default : BlueprintContent

Equations

• BlueprintGen.instInhabitedBlueprintContent.default = BlueprintGen.BlueprintContent.node default

def BlueprintGen.instReprBlueprintContent.repr : BlueprintContent → Nat → Std.Format

Equations

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

instance BlueprintGen.instReprBlueprintContent : Repr BlueprintContent

Equations

• BlueprintGen.instReprBlueprintContent = { reprPrec := BlueprintGen.instReprBlueprintContent.repr }

def BlueprintGen.BlueprintContent.declarationRange : BlueprintContent → Option Lean.DeclarationRange

Equations

• (BlueprintGen.BlueprintContent.node a).declarationRange = Option.map (fun (x : Lean.DeclarationLocation) => x.range) a.location
• (BlueprintGen.BlueprintContent.modDoc a).declarationRange = some a.declarationRange

def BlueprintGen.BlueprintContent.order (l r : BlueprintContent) : Bool

An order for blueprint contents, based on their declaration range.

Equations

• l.order r = match l.declarationRange, r.declarationRange with | some l, some r => l.pos.lt r.pos | some val, none => true | x, x_1 => false

def BlueprintGen.getMainModuleBlueprintContents : Lean.CoreM (Array BlueprintContent)

Get blueprint contents of the current module (this is for debugging).

Equations

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

def BlueprintGen.getBlueprintContents (module : Lean.Name) : Lean.CoreM (Array BlueprintContent)

Get blueprint contents of an imported module (this is for debugging).

Equations

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