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

Equations

• thm.declName = thm.expr.getAppFn.constName?

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

Equations

• Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry = { beq := Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry.beq }

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

Equations

• Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry.beq { appFn := a, thm := a_1 } { appFn := b, thm := b_1 } = (a == b && a_1 == b_1)
• Lean.Meta.Tactic.Cbv.instBEqCbvEvalEntry.beq x✝¹ x✝ = false

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalEntry.default = { appFn := default, thm := default }

@[implicit_reducible]

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

Equations

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

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.

Equations

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

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

• lemmas : NameMap Sym.Simp.Theorems

@[implicit_reducible]

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

Equations

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

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalState.default = { lemmas := default }

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

Equations

• s.addEntry e = { lemmas := s.lemmas.insert e.appFn (((s.lemmas.find? e.appFn).getD { }).insert e.thm) }

@[reducible, inline]

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

Equations

• Lean.Meta.Tactic.Cbv.CbvEvalExtension = Lean.SimpleScopedEnvExtension Lean.Meta.Tactic.Cbv.CbvEvalEntry Lean.Meta.Tactic.Cbv.CbvEvalState

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

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

Equations

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