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 : Lean.PHashMap Lake.Name (Array Lake.Name)

## Instances For

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

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

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.