Spec-theorem database used by mvcgen'. Mirrors the legacy SpecTheorems / SpecProof API from Lean.Elab.Tactic.Do.Attr but indexes specs in a Sym.DiscrTree keyed on the program's syntactic shape, with explicit SpecTheoremKind (triple vs. simp) and per-spec eta-potential metadata.

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

The kind of a spec theorem.

• triple (etaPotential : Nat := 0) : SpecTheoremKind

  A Hoare triple spec: ⦃P⦄ prog ⦃Q⦄. If etaPotential is non-zero, then the precondition contains meta variables that can be instantiated after applying mintro ∀s etaPotential many times.

• simp (etaArgs : Nat := 0) : SpecTheoremKind

  A simp/equational spec: lhs = rhs. The pattern is the LHS. When matched, the VCGen rewrites the program from lhs to rhs and continues. etaArgs is the number of extra arguments introduced by eta-expanding function-level equations (e.g., class projection unfold lemmas). These args need congrFun at instantiation time.

@[implicit_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheoremKind : Inhabited SpecTheoremKind

Equations

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

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

• pattern : Meta.Sym.Pattern

  Pattern for the program expression. This is the key used in the discrimination tree. If the proof has type ∀ a b c, Triple prog P Q, then the pattern is prog[a:=#2, b:=#1, c:=#0]. For simp specs with type ∀ a b c, lhs = rhs, the pattern is lhs[a:=#2, b:=#1, c:=#0].

• proof : SpecProof

  The proof for the theorem.

• kind : SpecTheoremKind

  The kind of spec theorem: triple or simp.

• priority : Nat

@[implicit_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheoremNew : Inhabited SpecTheoremNew

Equations

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

@[implicit_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheoremNew : BEq SpecTheoremNew

Equations

• Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheoremNew = { beq := fun (thm₁ thm₂ : Lean.Elab.Tactic.Do.SpecAttr.SpecTheoremNew) => thm₁.proof == thm₂.proof }

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

Like SpecProof.instantiate, but for simp specs also eta-expands function-level equations.

For unfold equations of class projections (e.g., MonadState.modifyGet.eq_1), the equation after forallMetaTelescope may be between functions rather than values: @modifyGet σ m self = self.3 : {α} → (σ → α × σ) → m α This method applies congrFun for each leading forall to reduce the equation to one between values of type m α, introducing fresh metavariables for the extra arguments. The number of extra args is stored in SpecTheoremKind.simp etaArgs.

Equations

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

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

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

@[implicit_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheoremsNew : Inhabited SpecTheoremsNew

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkTriplePatternFromExpr (expr : Expr) (levelParams : List Name := []) : Meta.Sym.SymM Meta.Sym.Pattern

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : Meta.Sym.SymM SpecTheoremNew

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew)

Create a SpecTheoremNew from a simp/equational declaration declName : ∀ xs, lhs = rhs. The pattern is keyed on lhs.

For unfold equations of class projections (e.g., MonadState.modifyGet.eq_1), the equation may be between functions rather than values. In that case, the pattern is eta-expanded so the discrimination tree key includes all arguments.

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : Meta.SimpTheorems) : Meta.Sym.SymM SpecTheoremsNew

Equations

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

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) : Meta.Sym.SymM (Except (Array SpecTheoremNew) SpecTheoremNew)

Look up SpecTheoremNews in the @[spec] database. Takes all specs that match the given program e and sorts by descending priority.

Equations

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