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.

• excludes : Array Lean.Name

  The set of nodes to exclude from uses.

• usesLabels : Array String

  Additional LaTeX labels of nodes that this node depends on.

• excludesLabels : Array String

  The set of labels to exclude from usesLabels.

• 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.

• proofExcludes : Array Lean.Name

  The set of nodes to exclude from proofUses.

• proofUsesLabels : Array String

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

• proofExcludesLabels : Array String

  The set of labels to exclude from proofUsesLabels.

• 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.

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

Equations

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

instance Architect.instReprConfig : Repr Config

Equations

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

def Architect.blueprintSingleUses : Lean.ParserDescr

Equations

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

def Architect.blueprintUses : Lean.ParserDescr

Equations

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

def Architect.elabBlueprintUses : Lean.TSyntax `Architect.blueprintUses → Lean.CoreM (Array Lean.Name × Array Lean.Name × Array String × Array String)

Returns array of (used names, excluded names, used labels, excluded labels).

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) (cfg : Config) (hasProof : Bool) : Lean.CoreM NodePart

Equations

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

def Architect.mkProofPart (_name : Lean.Name) (cfg : Config) : 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.