Commit 2023-04-13 22:33 94c39a2c

View on Github →

feat: ToExpr deriving handler (#3215) Add a deriving handler for ToExpr loosely modeled off the Repr one. Supports mutually recursive inductive types. Introduces a ToLevel typeclass for creating Level expressions that represent universe levels. This is used in the derived ToExpr instances to support some universe polymorphism.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/DeriveToExpr.lean

added def Mathlib.Deriving.ToExpr.fixIndType

added def Mathlib.Deriving.ToExpr.mkAppNTerm

added def Mathlib.Deriving.ToExpr.mkAuxFunction

added def Mathlib.Deriving.ToExpr.mkInstanceCmds

added def Mathlib.Deriving.ToExpr.mkLocalInstanceLetDecls

added def Mathlib.Deriving.ToExpr.mkMutualBlock

added def Mathlib.Deriving.ToExpr.mkToExprBody

added def Mathlib.Deriving.ToExpr.mkToExprHeader

added def Mathlib.Deriving.ToExpr.mkToExprInstanceCmds

added def Mathlib.Deriving.ToExpr.mkToExprInstanceHandler

added def Mathlib.Deriving.ToExpr.mkToLevelBinders

added def Mathlib.Deriving.ToExpr.mkToTypeExpr

Created Mathlib/Tactic/ToExpr.lean

Created Mathlib/Tactic/ToLevel.lean

added def Lean.ToLevel.imax

added def Lean.ToLevel.max

Created test/DeriveToExpr.lean

added inductive tests.A

added inductive tests.B

added inductive tests.Bar

added inductive tests.C

added inductive tests.D

added inductive tests.Foo

added inductive tests.MyMaybe

added def tests.boolFunHelper