Documentation

Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache

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

source
def Lean.Elab.Tactic.Do.Internal.VCGen.SpecTheoremNew.global? (specThm : SpecAttr.SpecTheoremNew) :
Option Name
Instances For
    source
    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.

    Instances For
      source
      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.

      Instances For