# Documentation

Lean.Meta.Eqns

Instances For

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

Instances For
• map :
Instances For
def Lean.Meta.getEqnsFor? (declName : Lake.Name) (nonRec : ) :

Return equation theorems for the given declaration. By default, we 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.

Instances For
Instances For

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

Instances For
def Lean.Meta.getUnfoldEqnFor? (declName : Lake.Name) (nonRec : ) :

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

Instances For