VCGenM-level cache wrappers around the SymM rule constructors in VCGen.RuleConstruction.

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleFromSpecCached (specThm : SpecAttr.SpecTheorem) (info : WPApp) : OptionT VCGenM Meta.Sym.BackwardRule

Cached version of spec rule construction.

Both Triple/⊑ wp and equality entries go through tryMkBackwardRuleFromSpec, which normalizes an equality spec to ⊑ wp form using the supplied wp metadata before building the rule.

Cache key: (proof key, instWP, excessArgs.size).

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleForSplitCached (splitInfo : SplitInfo) (info : WPApp) : VCGenM Meta.Sym.BackwardRule

Cached version of mkBackwardRuleForSplit.

Cache key: (splitter name, instWP, excessArgs.size).

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkLatticeOpRuleCached (rhs : Expr) (op : LatticeOp) : VCGenM Meta.Sym.BackwardRule

Cached construction of a lattice-split backward rule for the operator heading rhs. On a cache miss the rewrite and terminal sets are assembled from the built-in seeds and the operator's @[frameproc] contributions (fp?); a cache hit skips that work.

Cache key: the head … cₙ prefix built from the constant arguments (which the rule bakes in verbatim) and the argument count (which fixes the schematic operand and state count).

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkFrameBackwardRuleCached (op : Expr) (info : WPApp) : VCGenM Meta.Sym.BackwardRule

Cached version of mkFrameBackwardRule.

Cache key: (instWP, excessArgs.size) (the operator is determined by the monad).

Equations

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