@[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 name of the theorem used, the precomputed Theorem object and a name of the head function appearing on the left-hand side of the theorem.

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

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

Equations

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

@[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.instInhabitedCbvEvalEntry.default : CbvEvalEntry

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvEvalEntry.default = { origin := 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
• entries : NameMap (Array CbvEvalEntry)

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

Equations

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

@[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.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), entries := s.entries.insert e.appFn (((s.entries.find? e.appFn).getD ∅).push e) }

def Lean.Meta.Tactic.Cbv.CbvEvalState.erase (s : CbvEvalState) (declName : Name) : Option CbvEvalState

Erase a theorem from the state. Returns none if the theorem is not found.

Equations

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

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