opaque Lean.Elab.Tactic.Do.SpecAttr.mvcgenSimpExt : Meta.SimpExtension

This attribute should not be used directly. It is an implementation detail of the mvcgen tactic.

def Lean.Elab.Tactic.Do.SpecAttr.getSpecSimpTheorems : CoreM Meta.SimpTheorems

The simp set accumulated by the @[spec] attribute. (This does not include Hoare triple specs.) It is an implementation detail of the mvcgen tactic.

Equations

• Lean.Elab.Tactic.Do.SpecAttr.getSpecSimpTheorems = Lean.Elab.Tactic.Do.SpecAttr.mvcgenSimpExt.getTheorems

inductive Lean.Elab.Tactic.Do.SpecAttr.SpecProof : Type

• global (declName : Name) : SpecProof
• local (fvarId : FVarId) : SpecProof
• stx (id : Name) (ref : Syntax) (proof : Expr) : SpecProof

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof : Inhabited SpecProof

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof = { default := Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global default }

instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof : BEq SpecProof

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof = { beq := Lean.Elab.Tactic.Do.SpecAttr.beqSpecProof✝ }

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.key : SpecProof → Name

A unique identifier corresponding to the origin.

Equations

• (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global declName).key = declName
• (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local fvarId).key = fvarId.name
• (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.stx id ref proof).key = id

instance Lean.Elab.Tactic.Do.SpecAttr.instHashableSpecProof : Hashable SpecProof

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instHashableSpecProof = { hash := fun (sp : Lean.Elab.Tactic.Do.SpecAttr.SpecProof) => hash sp.key }

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.instantiate (proof : SpecProof) : MetaM (Array Expr × Array BinderInfo × Expr × Expr)

Equations

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

instance Lean.Elab.Tactic.Do.SpecAttr.instToMessageDataSpecProof : ToMessageData SpecProof

Equations

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

structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem : Type

• keys : Array Meta.DiscrTree.Key
• prog : Expr

  Expr key tested for matching, in ∀-quantified form. keys = (← mkPath (← forallMetaTelescope prog).2.2).

• proof : SpecProof

  The proof for the theorem.

• etaPotential : Nat

  If etaPotential is non-zero, then the precondition contains meta variables that can be instantiated after applying mintro ∀s etaPotential many times.

• priority : Nat

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem : Inhabited SpecTheorem

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem = { default := { keys := default, prog := default, proof := default, etaPotential := default, priority := default } }

instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem : BEq SpecTheorem

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem = { beq := Lean.Elab.Tactic.Do.SpecAttr.beqSpecTheorem✝ }

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecEntry : Type

Equations

• Lean.Elab.Tactic.Do.SpecAttr.SpecEntry = Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem

structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems : Type

• specs : Meta.DiscrTree SpecTheorem
• erased : PHashSet SpecProof

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems : Inhabited SpecTheorems

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems = { default := { specs := default, erased := default } }

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool

Equations

• d.isErased thmId = Lean.PersistentHashSet.contains d.erased thmId

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.eraseCore (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems

Equations

• d.eraseCore thmId = { specs := d.specs, erased := Lean.PersistentHashSet.insert d.erased thmId }

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecExtension : Type

Equations

• Lean.Elab.Tactic.Do.SpecAttr.SpecExtension = Lean.SimpleScopedEnvExtension Lean.Elab.Tactic.Do.SpecAttr.SpecEntry Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems

def Lean.Elab.Tactic.Do.SpecAttr.simpSPredConfig : Meta.ConfigWithKey

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.computeMVarBetaPotentialForSPred (xs : Array Expr) (σs e : Expr) : MetaM Nat

If σs : List Type, then e : SPred σs. Return the number of times e needs to be applied in order to assign closed solutions to meta variables.

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromConst (declName : Name) (prio : Nat := 1000) : MetaM SpecTheorem

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := 1000) : MetaM SpecTheorem

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := 1000) : MetaM SpecTheorem

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.addSpecTheoremEntry (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems

Equations

• Lean.Elab.Tactic.Do.SpecAttr.addSpecTheoremEntry d e = { specs := d.specs.insertCore e.keys e, erased := d.erased }

def Lean.Elab.Tactic.Do.SpecAttr.addSpecTheorem (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecExt : SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems

Equations

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

opaque Lean.Elab.Tactic.Do.SpecAttr.specAttr : SpecExtension

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecAttr (ext : SpecExtension) : AttributeImpl

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems

Equations

• ext.getTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift)

def Lean.Elab.Tactic.Do.SpecAttr.getSpecTheorems : CoreM SpecTheorems

Equations

• Lean.Elab.Tactic.Do.SpecAttr.getSpecTheorems = Lean.Elab.Tactic.Do.SpecAttr.specAttr.getTheorems