def Lean.Meta.GetEqnsFn : Type

Equations

• Lean.Meta.GetEqnsFn = (Lake.Name → Lean.MetaM (Option (Array Lake.Name)))

def Lean.Meta.registerGetEqnsFn (f : Lean.Meta.GetEqnsFn) : IO Unit

Register a new function for retrieving equation theorems. We generate equations theorems on demand, and they are generated by more than one module. For example, the structural and well-founded recursion modules generate them. Most recent getters are tried first.

A getter returns an Option (Array Name). The result is none if the getter failed. Otherwise, it is a sequence of theorem names where each one of them corresponds to an alternative. Example: the definition

def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs

should have two equational theorems associated with it

f [] = []

and

(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs

Equations

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

structure Lean.Meta.EqnsExtState : Type

• map : Lean.PHashMap Lake.Name (Array Lake.Name)
• mapInv : Lean.PHashMap Lake.Name Lake.Name

instance Lean.Meta.instInhabitedEqnsExtState : Inhabited Lean.Meta.EqnsExtState

Equations

• Lean.Meta.instInhabitedEqnsExtState = { default := { map := default, mapInv := default } }

opaque Lean.Meta.eqnsExt : Lean.EnvExtension Lean.Meta.EqnsExtState

def Lean.Meta.isEqnThm? (thmName : Lake.Name) : Lean.CoreM (Option Lake.Name)

Returns some declName if thmName is an equational theorem for declName.

Equations

• Lean.Meta.isEqnThm? thmName = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Meta.eqnsExt __do_lift).mapInv thmName)

def Lean.Meta.getEqnsFor? (declName : Lake.Name) (nonRec : optParam Bool false) : Lean.MetaM (Option (Array Lake.Name))

Returns equation theorems for the given declaration. By default, we do not create equation theorems for nonrecursive definitions. You can use nonRec := true to override this behavior, a dummy rfl proof is created on the fly.

Equations

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

def Lean.Meta.GetUnfoldEqnFn : Type

Equations

• Lean.Meta.GetUnfoldEqnFn = (Lake.Name → Lean.MetaM (Option Lake.Name))

def Lean.Meta.registerGetUnfoldEqnFn (f : Lean.Meta.GetUnfoldEqnFn) : IO Unit

Register a new function for retrieving a "unfold" equation theorem.

We generate this kind of equation theorem on demand, and it is generated by more than one module. For example, the structural and well-founded recursion modules generate it. Most recent getters are tried first.

A getter returns an Option Name. The result is none if the getter failed. Otherwise, it is a theorem name. Example: the definition

def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs

should have the theorem

(xs : Nat) →
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs

Equations

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

def Lean.Meta.getUnfoldEqnFor? (declName : Lake.Name) (nonRec : optParam Bool false) : Lean.MetaM (Option Lake.Name)

Return an "unfold" theorem for the given declaration. By default, we do not create unfold theorems for nonrecursive definitions. You can use nonRec := true to override this behavior.

Equations

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