structure Architect.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 String

  The names of nodes that this node depends on.

• latexEnv : String

  The LaTeX environment to use for this part.

def Architect.instInhabitedNodePart.default : NodePart

Equations

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

instance Architect.instInhabitedNodePart : Inhabited NodePart

Equations

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

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

Equations

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

instance Architect.instReprNodePart : Repr NodePart

Equations

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

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

Equations

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

instance Architect.instFromJsonNodePart : Lean.FromJson NodePart

Equations

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

instance Architect.instToJsonNodePart : Lean.ToJson NodePart

Equations

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

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

Equations

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

instance Architect.instToExprNodePart : Lean.ToExpr NodePart

Equations

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

def Architect.instToExprNodePart.toExpr : NodePart → Lean.Expr

Equations

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

structure Architect.Node : Type

A theorem or definition in the blueprint graph.

• name : Lean.Name

  The Lean name of the tagged constant.

• latexLabel : String

  The LaTeX label of the node. Multiple nodes can have the same label.

• 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 Architect.instInhabitedNode : Inhabited Node

Equations

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

def Architect.instInhabitedNode.default : Node

Equations

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

instance Architect.instReprNode : Repr Node

Equations

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

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

Equations

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

instance Architect.instFromJsonNode : Lean.FromJson Node

Equations

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

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

Equations

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

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

Equations

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

instance Architect.instToJsonNode : Lean.ToJson Node

Equations

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

def Architect.instToExprNode.toExpr : Node → Lean.Expr

Equations

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

instance Architect.instToExprNode : Lean.ToExpr Node

Equations

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

structure Architect.NodeWithPosextends Architect.Node : Type

• name : Lean.Name
• latexLabel : String
• 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.

def Architect.instInhabitedNodeWithPos.default : NodeWithPos

Equations

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

instance Architect.instInhabitedNodeWithPos : Inhabited NodeWithPos

Equations

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

instance Architect.instReprNodeWithPos : Repr NodeWithPos

Equations

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

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

Equations

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

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

Equations

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

opaque Architect.blueprintExt : Lean.NameMapExtension Node

Environment extension that stores the nodes of the blueprint.

@[reducible, inline]

abbrev Architect.LatexLabelToLeanNames.State : Type

Equations

• Architect.LatexLabelToLeanNames.State = Lean.SMap String (Array Lean.Name)

@[reducible, inline]

abbrev Architect.LatexLabelToLeanNames.Entry : Type

Equations

• Architect.LatexLabelToLeanNames.Entry = (String × Lean.Name)

opaque Architect.latexLabelToLeanNamesExt : Lean.SimplePersistentEnvExtension LatexLabelToLeanNames.Entry LatexLabelToLeanNames.State

def Architect.addLeanNameOfLatexLabel (env : Lean.Environment) (latexLabel : String) (name : Lean.Name) : Lean.Environment

Equations

• Architect.addLeanNameOfLatexLabel env latexLabel name = Lean.PersistentEnvExtension.addEntry Architect.latexLabelToLeanNamesExt env (latexLabel, name)

def Architect.getLeanNamesOfLatexLabel (env : Lean.Environment) (latexLabel : String) : Array Lean.Name

Equations

• Architect.getLeanNamesOfLatexLabel env latexLabel = Lean.SMap.findD (Architect.latexLabelToLeanNamesExt.getState env) latexLabel #[]

opaque Architect.blueprint.ignoreUnknownConstants : Lean.Option Bool

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