structure BlueprintGen.NodePart : Type

The statement or proof of a node.

• leanOk : Bool

  Whether the part is formalized without sorry in Lean.

• text : String

  The natural language description of this part.

• uses : Array Lean.Name

  The names of nodes that this node depends on.

• latexEnv : String

  The LaTeX environment to use for this part.

def BlueprintGen.instInhabitedNodePart.default : NodePart

Equations

• BlueprintGen.instInhabitedNodePart.default = { leanOk := default, text := default, uses := default, latexEnv := default }

instance BlueprintGen.instInhabitedNodePart : Inhabited NodePart

Equations

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

def BlueprintGen.instReprNodePart.repr : NodePart → Nat → Std.Format

Equations

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

instance BlueprintGen.instReprNodePart : Repr NodePart

Equations

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

def BlueprintGen.instFromJsonNodePart.fromJson : Lean.Json → Except String NodePart

Equations

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

instance BlueprintGen.instFromJsonNodePart : Lean.FromJson NodePart

Equations

• BlueprintGen.instFromJsonNodePart = { fromJson? := BlueprintGen.instFromJsonNodePart.fromJson }

def BlueprintGen.instToJsonNodePart.toJson : NodePart → Lean.Json

Equations

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

instance BlueprintGen.instToJsonNodePart : Lean.ToJson NodePart

Equations

• BlueprintGen.instToJsonNodePart = { toJson := BlueprintGen.instToJsonNodePart.toJson }

instance BlueprintGen.instToExprNodePart : Lean.ToExpr NodePart

Equations

• BlueprintGen.instToExprNodePart = { toExpr := BlueprintGen.instToExprNodePart.toExpr✝, toTypeExpr := Lean.Expr.const `BlueprintGen.NodePart [] }

structure BlueprintGen.Node : Type

A theorem or definition in the blueprint graph.

• name : Lean.Name

  The Lean name of the tagged constant.

• statement : NodePart

  The statement of this node.

• proof : Option NodePart

  The proof of this node.

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

instance BlueprintGen.instInhabitedNode : Inhabited Node

Equations

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

def BlueprintGen.instInhabitedNode.default : Node

Equations

• BlueprintGen.instInhabitedNode.default = { name := default, statement := default, proof := default, notReady := default, discussion := default, title := default }

def BlueprintGen.instReprNode.repr : Node → Nat → Std.Format

Equations

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

instance BlueprintGen.instReprNode : Repr Node

Equations

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

instance BlueprintGen.instFromJsonNode : Lean.FromJson Node

Equations

• BlueprintGen.instFromJsonNode = { fromJson? := BlueprintGen.instFromJsonNode.fromJson }

def BlueprintGen.instFromJsonNode.fromJson : Lean.Json → Except String Node

Equations

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

instance BlueprintGen.instToJsonNode : Lean.ToJson Node

Equations

• BlueprintGen.instToJsonNode = { toJson := BlueprintGen.instToJsonNode.toJson }

def BlueprintGen.instToJsonNode.toJson : Node → Lean.Json

Equations

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

instance BlueprintGen.instToExprNode : Lean.ToExpr Node

Equations

• BlueprintGen.instToExprNode = { toExpr := BlueprintGen.instToExprNode.toExpr✝, toTypeExpr := Lean.Expr.const `BlueprintGen.Node [] }

structure BlueprintGen.NodeWithPosextends BlueprintGen.Node : Type

• name : Lean.Name
• statement : NodePart
• proof : Option NodePart
• notReady : Bool
• discussion : Option Nat
• title : Option String
• hasLean : Bool

  Whether the node name is in the environment. This should always be true for nodes e.g. added by @[blueprint].

• location : Option Lean.DeclarationLocation

  The location (module & range) the node is defined in.

• file : Option System.FilePath

  The file the node is defined in.

instance BlueprintGen.instInhabitedNodeWithPos : Inhabited NodeWithPos

Equations

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

def BlueprintGen.instInhabitedNodeWithPos.default : NodeWithPos

Equations

• BlueprintGen.instInhabitedNodeWithPos.default = { toNode := default, hasLean := default, location := default, file := default }

instance BlueprintGen.instReprNodeWithPos : Repr NodeWithPos

Equations

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

def BlueprintGen.instReprNodeWithPos.repr : NodeWithPos → Nat → Std.Format

Equations

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

def BlueprintGen.Node.toNodeWithPos (node : Node) : Lean.CoreM NodeWithPos

Equations

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

opaque BlueprintGen.blueprintExt : Lean.NameMapExtension Node

Environment extension that stores the nodes of the blueprint.

opaque BlueprintGen.blueprint.ignoreUnknownConstants : Lean.Option Bool

def BlueprintGen.tryResolveConst (id : Lean.Ident) : Lean.CoreM Lean.Name

Resolves an identifier using realizeGlobalConstNoOverloadWithInfo. Ignores unknown constants if blueprint.ignoreUnknownConstants is true (default: false).

Equations

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