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

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

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

def Architect.instReprModuleDoc_architect.repr : Lean.ModuleDoc → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Architect.instReprModuleDoc_architect : Repr Lean.ModuleDoc

Equations

• Architect.instReprModuleDoc_architect = { reprPrec := Architect.instReprModuleDoc_architect.repr }

inductive Architect.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

def Architect.instInhabitedBlueprintContent.default : BlueprintContent

Equations

• Architect.instInhabitedBlueprintContent.default = Architect.BlueprintContent.node default

@[implicit_reducible]

instance Architect.instInhabitedBlueprintContent : Inhabited BlueprintContent

Equations

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

@[implicit_reducible]

instance Architect.instReprBlueprintContent : Repr BlueprintContent

Equations

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

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

Equations

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

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

Equations

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

def Architect.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 Architect.getMainModuleBlueprintContents : Lean.CoreM (Array BlueprintContent)

Get blueprint contents of the current module.

Equations

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

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

Get blueprint contents of an imported module. When blueprint.all is set, auto-nodes for the module's own declarations are included (this is the path used by lake build :blueprint).

Equations

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