Commit 2023-05-28 05:00 63c31ccb

View on Github →

feat: add compile_inductive% and compile_def% commands (#4097) Add a #compile inductive command to compile the recursors of an inductive type, which works by creating a recursive definition and using @[csimp].

Estimated changes

deleted theorem Quiver.Path.rec_eq_recC
deleted def List.recC.{u_1,
deleted theorem List.rec_eq_recC
deleted def Option.recC.{u_1,
deleted def Option.recOnC.{u_1,
deleted theorem Option.recOn_eq_recOnC
deleted theorem Option.rec_eq_recC
deleted def Tree.recOnC
deleted theorem Tree.recOn_Unit_eq_recOnC
deleted def Nat.recC.{u}
deleted theorem Nat.rec_eq_recC
deleted def Prod.recC
deleted theorem rec_eq_recC