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

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

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

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

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

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

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

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

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

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

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

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)

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

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

• priority : Nat

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

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

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

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

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

Equations

• d.insert e = { specs := Lean.Meta.Sym.insertPattern d.specs e.pattern e, erased := d.erased }

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 mvcgen''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.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.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