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.

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_reducible]

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

@[instance_reducible]

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

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

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

A unique identifier corresponding to the origin.

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.ofOrigin : Meta.Origin → Option SpecProof

Convert a simp Origin to a SpecProof.

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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_reducible]

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

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

@[instance_reducible]

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

@[reducible, inline]

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

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

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

@[instance_reducible]

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

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

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

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

@[reducible, inline]

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

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

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.

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

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

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

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

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

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

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

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

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

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

The kind of a spec theorem.

• triple : SpecTheoremKind

  A Hoare triple spec: ⦃P⦄ prog ⦃Q⦄.

• 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.

@[instance_reducible]

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

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

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

A unique identifier corresponding to the origin.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.ofOrigin : Meta.Origin → Option SpecProof

Convert a simp Origin to a SpecProof.

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

@[instance_reducible]

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.tripleToWpProof? (proof type : Expr) : MetaM (Option (Expr × Expr))

Normalises a specification proof so its conclusion is in pre ⊑ wp … form.

• Returns some for Triple proofs (rewriting via Triple.hwp) and proofs already in pre ⊑ wp … form (passed through unchanged).
• Returns none if type is neither shape; callers should throwError.

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

@[instance_reducible]

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

structure Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorem : 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 d e, ⦃P⦄ prog ⦃Q⦄ and only a, c and e occur in prog, then the pattern is prog[a:=#2, c:=#1, e:=#0]. For specs stated as pre ⊑ wp prog post epost, the pattern is keyed on prog.

• proof : SpecProof

  The proof for the theorem.

• kind : SpecTheoremKind

  The kind of spec theorem: triple or simp.

• conjunctivePre : Bool

  Whether the precondition is conjunctive in the spec's postconditions, so applying the spec directly carries any frame and vcgen skips the frame machinery. Opt out with a trivial Q = Q premise.

• priority : Nat

@[instance_reducible]

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

@[instance_reducible]

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

@[reducible, inline]

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.explicitSpecPrio : Nat

Priority for a spec named in a vcgen [...] argument list.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.starSpecPrio : Nat

Priority for a local hypothesis pulled into vcgen's spec set by *.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.unfoldSpecPrio : Nat

Priority for the equational and unfold specs a bracketed definition in a vcgen [...] list contributes.

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

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

@[instance_reducible]

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

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

Insert e, keeping the higher priority when a spec with the same proof is already stored.

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

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

@[reducible, inline]

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.eraseUnusedVarsFromPattern (p : Meta.Sym.Pattern) : Meta.Sym.Pattern

Drops pattern variables that the pattern expression does not depend on.

Sym.mkPatternFromExprWithKey/Sym.mkPatternFromDeclWithKey turn every leading ∀-binder of the source type into a pattern variable, even binders the selected key (e.g. the program of a Triple conclusion) never mentions. During matching those variables only ever become fresh metavariables (see Sym.mkPreResult); for instance binders they additionally trigger spurious trySynthInstance calls. This keeps only the variables that the pattern expression references, together with the transitive closure of variables their types depend on, and renumbers the remaining de Bruijn indices. varInfos? and checkTypeMask? are filtered to the surviving telescope; fnInfos, levelParams, and the discrimination-tree key are unchanged because the pattern expression's structure is untouched (bound variables are wildcards in the key).

Important: only use this when the matched arguments are not reused to rebuild a proof term, as Sym.BackwardRule/Sym.mkValue do — dropping variables would drop arguments those need. It is meant for databases such as vcgen's spec table, where the proof is re-elaborated independently of the pattern.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.progArgIdx? (declName : Name) : MetaM (Option Nat)

The application-argument index of declName's program parameter x, read from its signature.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.selectProg (type : Expr) : MetaM (Option Expr)

Selects the program a spec conclusion is keyed on: the program of a Triple, or the program inside the wp on the RHS of a pre ⊑ wp … entailment. Returns none if type is neither shape — e.g. a bare lhs ⊑ rhs whose RHS is not a wp application (an invariant entailment such as (I n h).inv … ⊑ Q n r.2, which can appear as an ordinary hypothesis but is not a spec). Callers use none to skip such non-spec hypotheses instead of failing.

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

Builds a Sym.Pattern keyed on the program selected by selectProg from a spec conclusion. The conclusion is assumed to already be a valid spec shape (checked by the caller via selectProg); a non-spec shape reaching here is a logic error and throws.

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

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

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheorem)

Create a SpecTheorem from a simp/equational declaration declName : ∀ xs, lhs = rhs, keyed on the LHS. Function-level equations (e.g. class projection unfold lemmas) are eta-expanded so the discrimination-tree key includes all arguments. Returns none for no-op equations whose LHS key is syntactically the RHS.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromSimpExpr? (ref : Syntax) (proof : Expr) (levelParams : List Name := []) (prio : Nat := 1000) : MetaM (Option SpecTheorem)

Create a SpecTheorem from an elaborated equational proof term proof : ∀ xs, lhs = rhs, keyed on the LHS. Mirrors mkSpecTheoremFromSimpDecl? for proofs supplied as terms rather than declaration names. Returns none for a no-op equation whose LHS key equals its RHS.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.unfoldSpecEqn? (declName : Name) : MetaM (Option Name)

The unfold theorem declName.eq_def through which a definition in a simp set's toUnfold rewrites, the spec-database counterpart of simp's delta unfolding. none for a recursive definition, whose unconditional unfolding would not terminate.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.simpSpecTheorems (entries : Array Meta.SimpEntry) (prio : Nat) : MetaM (Array SpecTheorem)

The spec theorems the simp entries entries contribute, the single place a vcgen [...] argument or an attribute [spec] f definition (through mkSimpEntryOfDeclToUnfold) turns into specs:

• each .thm entry, keyed on its left-hand side at prio, skipping wildcard-row equations guarded by an overlap hypothesis (as a spec such an equation matches any call and strands the hypothesis as a verification condition). A declaration equation is keyed via mkSpecTheoremFromSimpDecl?; an equation supplied as a vcgen [...] term carries its proof directly (mkSpecTheoremFromSimpExpr?),
• each .toUnfold definition through its unfold theorem f.eq_def (unfoldSpecEqn?) at priority 0, below every equation, so a call with an opaque discriminant still rewrites to the underlying match expression, which vcgen then splits. A single malformed entry is traced and skipped rather than aborting the set.

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

Register the equational lemmas of a @[spec]-annotated declaration as .simp entries with the given priority. An equational proposition is registered directly; a definition is registered via the specs its simp entries contribute (simpSpecTheorems). Anything else throws, since it cannot serve as a vcgen spec.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.specEraseProofs (declName : Name) : MetaM (Array SpecProof)

The spec proofs a @[spec] constant contributes to the database: the constant itself for a Triple/⊑ wp spec, the equation itself for an equational spec, or the specs its simp set contributes for a definition registered to unfold. Mirrors addSimpSpecTheoremsFromConst so [-foo] erases exactly the entries that annotating foo inserted.

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

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

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

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

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

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

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecAttr : AttributeImpl

opaque Lean.Elab.Tactic.Do.SpecAttr.specInvariantAttr : TagAttribute

Marks a type as an invariant type for the mvcgen tactic. Goals whose type is an application of a tagged type will be classified as invariants rather than verification conditions.

def Lean.Elab.Tactic.Do.SpecAttr.isSpecInvariantType (env : Environment) (ty : Expr) : Bool

Returns true if ty is an application of a type tagged with @[spec_invariant_type].