CompileInductive

📁 Source: Mathlib/Util/CompileInductive.lean

Statistics

Metric	Count
Definitions compileDefn, compileInductive, compileInductiveOnly, compileSizeOf, hasCSimpLemma, mkRecNames, «commandCompile_def%_», «commandCompile_inductive%_»	8
Theorems	0
Total	8

Mathlib.Util

Definitions

Name	Category	Theorems
compileDefn 📖	CompOp	—
compileInductive 📖	CompOp	—
compileInductiveOnly 📖	CompOp	—
compileSizeOf 📖	CompOp	—
hasCSimpLemma 📖	CompOp	—
mkRecNames 📖	CompOp	—
«commandCompile_def%_» 📖	CompOp	—
«commandCompile_inductive%_» 📖	CompOp	—

---

← Back to Index