ToExpr deriving handler

This module defines a ToExpr deriving handler for inductive types. It supports mutually inductive types as well.

The ToExpr deriving handlers support universe level polymorphism, via the Lean.ToLevel class. To use ToExpr in places where there is universe polymorphism, make sure a [ToLevel.{u}] instance is available, though be aware that the ToLevel mechanism does not support max or imax expressions.

Implementation note: this deriving handler was initially modeled after the Repr deriving handler, but

1. we need to account for universe levels,
2. the ToExpr class has two fields rather than one, and
3. we don't handle structures specially.