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

def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof.default : SpecProof

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq : SpecProof → SpecProof → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global a) (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global b) = (a == b)
• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local a) (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local b) = (a == b)
• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq x✝¹ x✝ = false

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

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.getProof : SpecProof → MetaM (List Name × Expr)

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.stx id ref proof).getProof = pure ([], proof)
• (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local fvarId).getProof = pure ([], Lean.mkFVar fvarId)

@[implicit_reducible]

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.

@[implicit_reducible]

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

def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem.default : SpecTheorem

Equations

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

@[implicit_reducible]

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

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem = { default := Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem.default }

@[implicit_reducible]

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

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq : SpecTheorem → SpecTheorem → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq x✝¹ x✝ = false

@[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

def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems.default : SpecTheorems

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

• d.insert e = { specs := d.specs.insertKeyValue e.keys e, erased := d.erased }

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.erase (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems

Equations

• d.erase 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.SpecExtension.addSpecTheoremFromConst (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit

Equations

• ext.addSpecTheoremFromConst declName prio attrKind = do let thm ← Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromConst declName prio Lean.ScopedEnvExtension.add ext thm attrKind

def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.addSpecTheoremFromLocal (ext : SpecExtension) (fvar : FVarId) (prio : Nat := 1000) : MetaM Unit

Equations

• ext.addSpecTheoremFromLocal fvar prio = do let thm ← Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromLocal fvar prio Lean.ScopedEnvExtension.add ext thm Lean.AttributeKind.local

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