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

Get or create cached Theorems for function equations. Retrieves equations via getEqnsFor? and caches the resulting Theorems object.

• 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 }

@[instance_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.