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.

def Mathlib.Deriving.ToExpr.mkToExprHeader (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM Lean.Elab.Deriving.Header

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

def Mathlib.Deriving.ToExpr.mkAppNTerm (f : Lean.Term) (args : Array Lean.Term) : Lean.MetaM Lean.Term

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.

def Mathlib.Deriving.ToExpr.mkToExprBody (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) : Lean.Elab.TermElabM Lean.Term

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.

def Mathlib.Deriving.ToExpr.mkToExprBody.mkAlts (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (auxFunName : Lean.Name) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))

Create the match cases, one per constructor.

Equations

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

def Mathlib.Deriving.ToExpr.mkToTypeExpr (argNames : Array Lean.Name) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM Lean.Term

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.

def Mathlib.Deriving.ToExpr.mkLocalInstanceLetDecls (ctx : Lean.Elab.Deriving.Context) (argNames : Array Lean.Name) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.letDecl))

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.

def Mathlib.Deriving.ToExpr.fixIndType (indVal : Lean.InductiveVal) (t : Lean.Term) : Lean.Elab.TermElabM Lean.Term

Fix the output of mkInductiveApp to explicitly reference universe levels.

Equations

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

def Mathlib.Deriving.ToExpr.mkToLevelBinders (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Elab.Deriving.instBinderF)

Make ToLevel instance binders for all the level variables.

Equations

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

def Mathlib.Deriving.ToExpr.mkAuxFunction (ctx : Lean.Elab.Deriving.Context) (i : Nat) : Lean.Elab.TermElabM Lean.Command

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.

def Mathlib.Deriving.ToExpr.mkMutualBlock (ctx : Lean.Elab.Deriving.Context) : Lean.Elab.TermElabM Lean.Syntax

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.

def Mathlib.Deriving.ToExpr.mkInstanceCmds (ctx : Lean.Elab.Deriving.Context) (typeNames : Array Lean.Name) : Lean.Elab.TermElabM (Array Lean.Command)

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.

def Mathlib.Deriving.ToExpr.mkToExprInstanceCmds (declNames : Array Lean.Name) : Lean.Elab.TermElabM (Array Lean.Syntax)

Returns all the commands generated by mkMutualBlock and mkInstanceCmds.

Equations

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

def Mathlib.Deriving.ToExpr.mkToExprInstanceHandler (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

The main entry point to the ToExpr derive handler.

Equations

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