structure BlueprintGen.Config : Type

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

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

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

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

• trace : Bool

  Enable debugging.

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

Equations

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

instance BlueprintGen.instReprConfig : Repr Config

Equations

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

def BlueprintGen.blueprintHasProofOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintProofOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintUsesOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintProofUsesOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintNotReadyOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintDiscussionOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintLatexEnvOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintOption : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprintOptions : Lean.ParserDescr

Equations

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

def BlueprintGen.blueprint : Lean.ParserDescr

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

You may optionally add:

• "Title": The title of the node in LaTeX.
• hasProof := true: If the node has a proof (default: true if the node is a theorem).
• proof := /-- ... -/: The proof of the node in text.
• uses := [a, b]: The dependencies of the node (default: inferred from the used constants).
• proofUses := [a, b]: The dependencies of the proof of the node (default: inferred from the used constants).
• 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 blueprint-gen.

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 BlueprintGen.attrBlueprint?_ : Lean.ParserDescr

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

You may optionally add:

• "Title": The title of the node in LaTeX.
• hasProof := true: If the node has a proof (default: true if the node is a theorem).
• proof := /-- ... -/: The proof of the node in text.
• uses := [a, b]: The dependencies of the node (default: inferred from the used constants).
• proofUses := [a, b]: The dependencies of the proof of the node (default: inferred from the used constants).
• 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 blueprint-gen.

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

Whether a node has a proof part.

Equations

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

def BlueprintGen.usedConstants (name : Lean.Name) : Lean.CoreM (Lean.NameSet × Lean.NameSet)

Returns a pair of sets (constants used by statement, constants used by proof). They are disjoint except that possibly both contain sorryAx.

Equations

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

def BlueprintGen.mkStatementPart (name : Lean.Name) (cfg : Config) (hasProof : Bool) (used : Lean.NameSet) : Lean.CoreM NodePart

Equations

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

def BlueprintGen.mkProofPart (name : Lean.Name) (cfg : Config) (used : Lean.NameSet) : Lean.CoreM NodePart

Equations

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

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

Equations

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

partial def BlueprintGen.checkCyclicUses (newName : Lean.Name) (node : Node) (visited : Lean.NameSet := ∅) (path : Array Lean.Name := #[]) : Lean.CoreM Unit

Raises an error if newName occurs in the (irreflexive transitive) dependencies of node. 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.)