Def Mathlib.Util.compileInductive

Modification history

2023-06-23 04:45

Mathlib/Util/CompileInductive.lean

fix: compile inductives recursively (#5039) …

Deleted Mathlib.Util.compileInductive View on Github →

2023-05-28 05:00

Mathlib/Util/CompileInductive.lean

feat: add `compile_inductive%` and `compile_def%` commands (#4097) …

Added Mathlib.Util.compileInductive View on Github →