- addMatchers : Array (Lean.MetaM Unit)
As part of the inductive predicates case, we keep adding more and more discriminants from the local context and build up a bigger matcher application until we reach a fixed point. As a side-effect, this creates matchers. Here we capture all these side-effects, because the construction rolls back any changes done to the environment and the side-effects need to be replayed.

## Instances For

## Instances For

## Equations

- Lean.Elab.Structural.instInhabitedM = { default := Lean.throwError (Lean.toMessageData "failed") }

## Equations

- Lean.Elab.Structural.run x s = StateRefT'.run x s

## Instances For

Return true iff `e`

contains an application `recFnName .. t ..`

where the term `t`

is
the argument we are trying to recurse on, and it contains loose bound variables.

We use this test to decide whether we should process a matcher-application as a regular
application or not. That is, whether we should push the `below`

argument should be affected by the matcher or not.
If `e`

does not contain an application of the form `recFnName .. t ..`

, then we know
the recursion doesn't depend on any pattern variable in this matcher.

## Equations

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

## Instances For

Lets say we have `n`

mutually recursive functions whose recursive arguments are from a group
of `m`

mutually inductive data types. This mapping does not have to be one-to-one: for one type
there can be zero, one or more functions. We use the logic in the `FunPacker`

modules to combine
the bodies (and motives) of multiple such functions.

Therefore we have to take the `n`

functions, group them by their recursive argument's type,
and for each such type, keep track of the order of the functions.

We represent these positions as an `Array (Array Nat)`

. We have that

`positions.size = indInfo.numTypeFormers`

`positions.flatten`

is a permutation of`[0:n]`

, so each of the`n`

functions has exactly one position, and each position refers to one of the`n`

functions.- if
`k ∈ positions[i]`

then the recursive argument of function`k`

is has type`indInfo.all[i]`

(or corresponding nested inductive type)

## Equations

## Instances For

The number of indices in the array.

## Equations

## Instances For

Groups the `xs`

by their `f`

value, and puts these groups into the order given by `ys`

.

## Equations

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

## Instances For

Let `positions.size = ys.size`

and `positions.numIndices = xs.size`

. Maps `f`

over each `y`

in `ys`

,
also passing in those elements `xs`

that belong to that are those elements of `xs`

that belong to
`y`

according to `positions`

.

## Equations

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