Documentation

Lean.Meta.Tactic.Cbv.TheoremsLookup

Cached Theorem Lookup #

Per-function cache of Sym.Simp.Theorem objects for equation theorems, unfold equations, and match equations. Avoids repeated mkTheoremFromDecl calls (which involve pattern extraction and discrimination tree insertion).

source
structure Lean.Meta.Tactic.Cbv.CbvTheoremsLookupState :
Type
Instances For
    source
    def Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState.default :
    CbvTheoremsLookupState
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState :
      Inhabited CbvTheoremsLookupState
      source
      def Lean.Meta.Tactic.Cbv.getEqnTheorems (fnName : Name) :
      MetaM Sym.Simp.Theorems
      Instances For
        source
        def Lean.Meta.Tactic.Cbv.getUnfoldTheorem (fnName : Name) :
        MetaM (Option Sym.Simp.Theorem)
        Instances For
          source
          def Lean.Meta.Tactic.Cbv.getMatchTheorems (matcherName : Name) :
          MetaM Sym.Simp.Theorems
          Instances For