## Equations

## 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
```

## Equations

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

## Instances For

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

## Instances For

## Equations

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

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)

## Instances For

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.

## Instances For

## Equations

## 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
```

## Equations

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

## Instances For

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.