Here we implement docstrings but for proofs.

@[reducible, inline]

abbrev BlueprintGen.ProofDocString.State : Type

Equations

• BlueprintGen.ProofDocString.State = Lean.SMap Lean.Name (Array String)

@[reducible, inline]

abbrev BlueprintGen.ProofDocString.Entry : Type

Equations

• BlueprintGen.ProofDocString.Entry = (Lean.Name × String)

opaque BlueprintGen.ProofDocString.proofDocStringExt : Lean.SimplePersistentEnvExtension Entry State

def BlueprintGen.addProofDocString (env : Lean.Environment) (name : Lean.Name) (doc : String) : Lean.Environment

Equations

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

def BlueprintGen.getProofDocString (env : Lean.Environment) (name : Lean.Name) : Array String

Equations

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

def BlueprintGen.tacticDocComment : Lean.ParserDescr

Equations

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

We implement the blueprint_using and sorry_using tactics that declares used constants.

@[reducible, inline]

abbrev BlueprintGen.ProofUsing.State : Type

Equations

• BlueprintGen.ProofUsing.State = Lean.SMap Lean.Name (Array Lean.Name)

@[reducible, inline]

abbrev BlueprintGen.ProofUsing.Entry : Type

Equations

• BlueprintGen.ProofUsing.Entry = (Lean.Name × Lean.Name)

opaque BlueprintGen.ProofUsing.proofUsingExt : Lean.SimplePersistentEnvExtension Entry State

def BlueprintGen.«tacticBlueprint_using[_,,]» : Lean.ParserDescr

blueprint_using [a, b] adds a and b as dependencies for the blueprint metadata.

It is basically the same as let := a; let := b.

Equations

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

def BlueprintGen.tacticSorryUsing : Lean.ParserDescr

sorry_using [a, b] is the same as sorry, but adds a and b as dependencies for the blueprint metadata.

It is basically similar to let := a; let := b; sorry.

Equations

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

def BlueprintGen.termSorryUsing : Lean.ParserDescr

sorry_using [a, b] is the same as sorry, but adds a and b as dependencies for the blueprint metadata.

It is basically similar to let := a; let := b; sorry.

Equations

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