Spec-theorem database used by vcgen. The @[spec] attribute already stores Std.Internal.Do specs as pattern-keyed SpecTheorems (see Lean.Elab.Tactic.Do.Attr); this module adds the operations the VC generator needs on top: instantiating a spec to pre ⊑ wp … form, folding a vcgen [...] call's simp-style arguments into the same database, and looking up the specs matching a program.

def Lean.Meta.Sym.Pattern.shareCommon (p : Pattern) : SymM Pattern

Internalizes the pattern's expressions into the current SymM share table.

A pattern is built in MetaM, outside the SymM thread whose table the targets are internalized into, so its closed subterms (the instance telescope of a wp application, for example) are structurally equal to but distinct from the targets'. Internalizing the pattern once makes those subterms pointer-equal to every target internalized afterwards, so matching them is O(1).

Equations

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

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

Instantiates a spec theorem's proof.

Hoare triple and ⊑ wp specs are normalised to pre ⊑ wp … form via tripleToWpProof?. Simp specs keep the raw lhs = rhs equality, but eta-expand 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.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorem.global? (specThm : SpecTheorem) : Option Name

The declaration name of a global spec theorem, none for local/syntactic specs.

Equations

• specThm.global? = match specThm.proof with | Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.global decl => some decl | x => none

def Lean.Elab.Tactic.Do.Internal.VCGen.addSimpSpecs (database : SpecAttr.SpecTheorems) (simpThms : Meta.SimpTheorems) : MetaM SpecAttr.SpecTheorems

Extend the spec database with the specs a vcgen [...] call's simp-style arguments contribute (simpSpecTheorems over the simpThms that mkSimpContext collected).

Hoare triple and ⊑ wp specs are already in database: the attribute stores them pattern-keyed at annotation time.

Equations

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems.findSpecs (database : SpecTheorems) (e : Expr) : Meta.Sym.SymM (Array SpecTheorem)

Look up SpecTheorems in the @[spec] database. Takes all specs the discrimination tree holds for the program e and sorts by descending priority.

Equations

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