# A `ToExpr`

derive handler #

This module defines a `ToExpr`

derive handler for inductive types. It supports mutually inductive
types as well.

The `ToExpr`

derive handlers support universe level polymorphism. This is implemented using the
`Lean.ToLevel`

class. To use `ToExpr`

in places where there is universe polymorphism, make sure
to have a `[ToLevel.{u}]`

instance available.

**Warning:** Import `Mathlib.Tactic.ToExpr`

instead of this one. This ensures that you are using
the universe polymorphic `ToExpr`

instances that override the ones from Lean 4 core.

Implementation note: this derive handler was originally modeled after the `Repr`

derive handler.

Specialization of `Lean.Elab.Deriving.mkHeader`

for `ToExpr`

.

## Equations

- Mathlib.Deriving.ToExpr.mkToExprHeader indVal = do let header ← Lean.Elab.Deriving.mkHeader `Lean.ToExpr 1 indVal pure header

## Instances For

Give a term that is equivalent to `(term| mkAppN $f #[$args,*])`

.
As an optimization, `mkAppN`

is pre-expanded out to use `Expr.app`

directly.

## Equations

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

## Instances For

Create the body of the `toExpr`

function
for the `ToExpr`

instance, which is a `match`

expression
that calls `toExpr`

and `toTypeExpr`

to assemble an expression for a given term.
For recursive inductive types, `auxFunName`

refers to the `ToExpr`

instance
for the current type.
For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`

.

## Equations

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

## Instances For

Create the `match`

cases, one per constructor.

## Equations

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

## Instances For

Create the body of the `toTypeExpr`

function for the `ToExpr`

instance.
Calls `toExpr`

and `toTypeExpr`

to the arguments to the type constructor.

## Equations

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

## Instances For

For mutually recursive inductive types, the strategy is to have local `ToExpr`

instances in scope
for each of the inductives when defining each instance.
This way, each instance can freely use `toExpr`

and `toTypeExpr`

for each of the other types.

Note that each instance gets its own definition of each of the others' `toTypeExpr`

fields.
(This is working around the fact that the `Deriving.Context`

API assumes
that each instance in mutual recursion only has a single auxiliary definition.
There are other ways to work around it, but `toTypeExpr`

implementations
are very simple, so duplicating them seemed to be OK.)

## Equations

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

## Instances For

Fix the output of `mkInductiveApp`

to explicitly reference universe levels.

## Equations

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

## Instances For

Make `ToLevel`

instance binders for all the level variables.

## Equations

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

## Instances For

Make a `toExpr`

function for the given inductive type.
The implementations of each `toExpr`

function for a (mutual) inductive type
are given as top-level private definitions.
These end up being assembled into `ToExpr`

instances in `mkInstanceCmds`

.
For mutual inductive types,
then each of the other types' `ToExpr`

instances are provided as local instances,
to wire together the recursion (this necessitates these auxiliary definitions being `partial`

).

## Equations

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

## Instances For

Create all the auxiliary functions using `mkAuxFunction`

for the (mutual) inductive type(s).
Wraps the resulting definition commands in `mutual ... end`

.

## Equations

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

## Instances For

Assuming all of the auxiliary definitions exist, create all the `instance`

commands
for the `ToExpr`

instances for the (mutual) inductive type(s).

## Equations

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

## Instances For

Returns all the commands generated by `mkMutualBlock`

and `mkInstanceCmds`

.

## Equations

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

## Instances For

The main entry point to the `ToExpr`

derive handler.

## Equations

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