VCGenM-level cache wrappers around the SymM rule constructors in VCGen.RuleConstruction. The cache key is (declName, m, excessArgs.size).

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

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleFromSpecCached (specThm : SpecAttr.SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : VCGenM Meta.Sym.BackwardRule

See the documentation for mkBackwardRuleFromSpec and mkBackwardRuleFromSimpSpec.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : VCGenM Meta.Sym.BackwardRule

Creates and caches a backward rule for splitting ite, dite, or matchers.

Equations

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