Here we implement docstrings but for proofs.

@[reducible, inline]

abbrev Architect.ProofDocString.State : Type

Equations

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

@[reducible, inline]

abbrev Architect.ProofDocString.Entry : Type

Equations

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

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

The environment extension that stores proof docstrings.

def Architect.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 Architect.getProofDocString (env : Lean.Environment) (name : Lean.Name) : String

Equations

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

def Architect.tacticDocComment : Lean.ParserDescr

Equations

• Architect.tacticDocComment = Lean.ParserDescr.node `Architect.tacticDocComment 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `plainDocComment) (Lean.ParserDescr.cat `tactic 0))

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

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