@[cbv_eval] Attribute and Extension

Environment extension for user-provided cbv rewrite rules. Each theorem is converted to a Sym.Simp.Theorem (precomputed Pattern + DiscrTree key) and indexed by the head constant on its LHS.

@[cbv_eval ←] inverts the theorem: an auxiliary lemma with swapped sides is created via mkAuxLemma.

def Lean.Meta.Sym.Simp.Theorem.declName (thm : Theorem) : Option Name

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

Entry of the CbvEvalExtension. Consists of the precomputed Theorem object and a name of the head function appearing on the left-hand side of the theorem.

• appFn : Name
• thm : Sym.Simp.Theorem

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry : BEq CbvEvalEntry

def Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry.beq : CbvEvalEntry → CbvEvalEntry → Bool

def Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalEntry.default : CbvEvalEntry

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalEntry : Inhabited CbvEvalEntry

def Lean.Meta.Tactic.Cbv.mkCbvTheoremFromConst (declName : Name) (inv : Bool := false) : MetaM CbvEvalEntry

Create a CbvEvalEntry from a theorem declaration. When inv = true, creates an auxiliary lemma with swapped sides so the theorem can be used for right-to-left rewriting.

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

• lemmas : NameMap Sym.Simp.Theorems

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalState : Inhabited CbvEvalState

def Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalState.default : CbvEvalState

def Lean.Meta.Tactic.Cbv.CbvEvalState.addEntry (s : CbvEvalState) (e : CbvEvalEntry) : CbvEvalState

@[reducible, inline]

abbrev Lean.Meta.Tactic.Cbv.CbvEvalExtension : Type

opaque Lean.Meta.Tactic.Cbv.cbvEvalExt : CbvEvalExtension

def Lean.Meta.Tactic.Cbv.getCbvEvalLemmas (target : Name) : CoreM (Option Sym.Simp.Theorems)