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_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 }

@[instance_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.ofOrigin : Meta.Origin → Option SpecProof

Convert a simp Origin to a SpecProof.

Equations

• Lean.Elab.Tactic.Do.SpecAttr.SpecProof.ofOrigin (Lean.Meta.Origin.decl declName post inv) = some (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global declName)
• Lean.Elab.Tactic.Do.SpecAttr.SpecProof.ofOrigin (Lean.Meta.Origin.fvar fvarId) = some (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local fvarId)
• Lean.Elab.Tactic.Do.SpecAttr.SpecProof.ofOrigin x✝ = none

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)

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

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

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

A unique identifier corresponding to the origin.

Equations

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

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

Convert a simp Origin to a SpecProof.

Equations

• Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.ofOrigin (Lean.Meta.Origin.decl declName post inv) = some (Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.global declName)
• Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.ofOrigin (Lean.Meta.Origin.fvar fvarId) = some (Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.local fvarId)
• Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.ofOrigin x✝ = none

def Lean.Elab.Tactic.Do.Internal.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.Internal.SpecAttr.SpecProof.stx id ref proof).getProof = pure ([], proof)
• (Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.local fvarId).getProof = pure ([], Lean.mkFVar fvarId)

@[instance_reducible]

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

Equations

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

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.

Equations

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

def Lean.Elab.Tactic.Do.Internal.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_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

• Lean.Elab.Tactic.Do.Internal.SpecAttr.instBEqSpecTheorem = { beq := fun (a b : Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorem) => a.proof == b.proof }

@[reducible, inline]

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

Equations

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

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

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

Equations

• Lean.Elab.Tactic.Do.Internal.SpecAttr.explicitSpecPrio = 10000 + 3000

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

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

Equations

• Lean.Elab.Tactic.Do.Internal.SpecAttr.starSpecPrio = 10000 + 2000

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

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

Equations

• Lean.Elab.Tactic.Do.Internal.SpecAttr.unfoldSpecPrio = 10000 + 1000

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

Equations

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

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.

Equations

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

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

Equations

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

def Lean.Elab.Tactic.Do.Internal.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.Internal.SpecAttr.SpecExtension : Type

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension.addSpecTheoremFromConst (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.Internal.SpecAttr.SpecExtension.addSpecTheoremFromLocal (ext : SpecExtension) (fvar : FVarId) (prio : Nat := 1000) : MetaM Unit

Equations

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

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

Equations

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

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

def Lean.Elab.Tactic.Do.Internal.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.Internal.SpecAttr.getSpecTheorems : CoreM SpecTheorems

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Do.SpecAttr.isSpecInvariantType env ty = match ty.getAppFn with | Lean.Expr.const name us => Lean.Elab.Tactic.Do.SpecAttr.specInvariantAttr.hasTag env name | x => false