Def Mathlib.Util.mkRecNames

Modification history

2023-05-28 05:00
Mathlib/Util/CompileInductive.lean
feat: add `compile_inductive%` and `compile_def%` commands (#4097) …
Added Mathlib.Util.mkRecNamesView on Github →