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

structure Lean.Meta.Tactic.Cbv.CbvTheoremsLookupState : Type

• eqnTheorems : PHashMap Name Sym.Simp.Theorems
• unfoldTheorems : PHashMap Name Sym.Simp.Theorem
• matchTheorems : PHashMap Name Sym.Simp.Theorems

def Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState.default : CbvTheoremsLookupState

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState.default = { eqnTheorems := default, unfoldTheorems := default, matchTheorems := default }

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState : Inhabited CbvTheoremsLookupState

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvTheoremsLookupState.default }

def Lean.Meta.Tactic.Cbv.getEqnTheorems (fnName : Name) : MetaM Sym.Simp.Theorems

Equations

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

def Lean.Meta.Tactic.Cbv.getUnfoldTheorem (fnName : Name) : MetaM (Option Sym.Simp.Theorem)

Equations

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

def Lean.Meta.Tactic.Cbv.getMatchTheorems (matcherName : Name) : MetaM Sym.Simp.Theorems

Equations

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