structure Architect.Config : Type

Config is the type of arguments that can be provided to blueprint.

• statement : Option String

  The statement of the node in text.

• hasProof : Option Bool

  By default, only theorems have separate proof parts. This option overrides this behavior.

• proof : Option String

  The proof of the node in text. Uses proof docstrings if not present.

• uses : Array Lean.Name

  The set of nodes that this node depends on. Infers from the constant if not present.

• usesRaw : Array String

  Additional raw labels of nodes that this node depends on.

• proofUses : Array Lean.Name

  The set of nodes that the proof of this node depends on. Infers from the constant's value if not present.

• proofUsesRaw : Array String

  Additional raw labels of nodes that the proof of this node depends on.

• notReady : Bool

  The surrounding environment is not ready to be formalized, typically because it requires more blueprint work.

• discussion : Option Nat

  A GitHub issue number where the surrounding definition or statement is discussed.

• title : Option String

  The short title of the node in LaTeX.

• latexEnv : Option String

  The LaTeX environment to use for the node.

• latexLabel : Option String

  The LaTeX label to use for the node.

• trace : Bool

  Enable debugging.

instance Architect.instReprConfig : Repr Config

Equations

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

def Architect.instReprConfig.repr : Config → Nat → Std.Format

Equations

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

def Architect.blueprintStatementOption : Lean.ParserDescr

Equations

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

def Architect.blueprintHasProofOption : Lean.ParserDescr

Equations

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

def Architect.blueprintProofOption : Lean.ParserDescr

Equations

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

def Architect.blueprintUsesOption : Lean.ParserDescr

Equations

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

def Architect.blueprintProofUsesOption : Lean.ParserDescr

Equations

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

def Architect.blueprintTitleOption : Lean.ParserDescr

Equations

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

def Architect.blueprintNotReadyOption : Lean.ParserDescr

Equations

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

def Architect.blueprintDiscussionOption : Lean.ParserDescr

Equations

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

def Architect.blueprintLatexEnvOption : Lean.ParserDescr

Equations

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

def Architect.blueprintLatexLabelOption : Lean.ParserDescr

Equations

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

def Architect.blueprintOption : Lean.ParserDescr

Equations

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

def Architect.blueprintOptions : Lean.ParserDescr

Equations

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

def Architect.blueprint : Lean.ParserDescr

The blueprint attribute tags a constant to add to the blueprint.

You may optionally add:

• "latex-label": The LaTeX label to use for the node (default: the Lean name).
• statement := /-- ... -/: The statement of the node in LaTeX.
• hasProof := true: If the node has a proof part (default: true if the node is a theorem).
• proof := /-- ... -/: The proof of the node in LaTeX (default: the docstrings in proof tactics).
• uses := [a, "b"]: The dependencies of the node, as Lean constants or LaTeX labels (default: inferred from the used constants).
• proofUses := [a, "b"]: The dependencies of the proof of the node, as Lean constants or LaTeX labels (default: inferred from the used constants).
• title := "Title": The title of the node in LaTeX.
• notReady := true: Whether the node is not ready.
• discussion := 123: The discussion issue number of the node.
• latexEnv := "lemma": The LaTeX environment to use for the node (default: "theorem" or "definition").

For more information, see LeanArchitect.

Use blueprint? to show the raw data of the added node.

Equations

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

def Architect.attrBlueprint?_ : Lean.ParserDescr

The blueprint attribute tags a constant to add to the blueprint.

You may optionally add:

• "latex-label": The LaTeX label to use for the node (default: the Lean name).
• statement := /-- ... -/: The statement of the node in LaTeX.
• hasProof := true: If the node has a proof part (default: true if the node is a theorem).
• proof := /-- ... -/: The proof of the node in LaTeX (default: the docstrings in proof tactics).
• uses := [a, "b"]: The dependencies of the node, as Lean constants or LaTeX labels (default: inferred from the used constants).
• proofUses := [a, "b"]: The dependencies of the proof of the node, as Lean constants or LaTeX labels (default: inferred from the used constants).
• title := "Title": The title of the node in LaTeX.
• notReady := true: Whether the node is not ready.
• discussion := 123: The discussion issue number of the node.
• latexEnv := "lemma": The LaTeX environment to use for the node (default: "theorem" or "definition").

For more information, see LeanArchitect.

Use blueprint? to show the raw data of the added node.

Equations

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

def Architect.elabBlueprintConfig : Lean.Syntax → Lean.CoreM Config

Elaborates the configuration options for blueprint.

Equations

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

def Architect.hasProof (name : Lean.Name) (cfg : Config) : Lean.CoreM Bool

Whether a node has a proof part.

Equations

• Architect.hasProof name cfg = do let __do_lift ← Lean.getEnv pure (cfg.hasProof.getD (cfg.proof.isSome || Lean.wasOriginallyTheorem __do_lift name))

def Architect.mkStatementPart (_name : Lean.Name) (latexLabel : String) (cfg : Config) (hasProof : Bool) (used : Lean.NameSet) : Lean.CoreM NodePart

Equations

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

def Architect.mkProofPart (name : Lean.Name) (latexLabel : String) (cfg : Config) (used : Lean.NameSet) : Lean.CoreM NodePart

Equations

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

def Architect.mkNode (name : Lean.Name) (cfg : Config) : Lean.CoreM Node

Equations

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

opaque Architect.blueprint.checkCyclicUses : Lean.Option Bool

partial def Architect.checkCyclicUses {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (newLabel label : String) (visited : Std.HashSet String := ∅) (path : Array String := #[]) : m Unit

Raises an error if newLabel occurs in the (irreflexive transitive) dependencies of label. If ignored, this would create a cycle and then an error during leanblueprint web.

(Note: this check will only raise an error if blueprint.ignoreUnknownConstants is true, which may permit cyclic dependencies.)