# Define the `compile_inductive%` command. #

The command `compile_inductive% Foo` adds compiled code for the recursor `Foo.rec`, working around a bug in the core Lean compiler which does not support recursors.

For technical reasons, the recursor code generated by `compile_inductive%` unfortunately evaluates the base cases eagerly. That is, `List.rec (unreachable!) (fun _ _ _ => 42) [42]` will panic.

Similarly, `compile_def% Foo.foo` adds compiled code for definitions when missing. This can be the case for type class projections, or definitions like `List._sizeOf_1`.

source
def Mathlib.Util.mkRecNames (all : List Lean.Name) (numMotives : Nat) :
List Lean.Name

Returns the names of the recursors for a nested or mutual inductive, using the `all` and `numMotives` arguments from `RecursorVal`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Util.compileDefn (dv : Lean.DefinitionVal) :
Lean.MetaM Unit

Compile the definition `dv` by adding a second definition `dv✝` with the same body, and registering a `csimp`-lemma `dv = dv✝`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Util.hasCSimpLemma (env : Lean.Environment) (n : Lean.Name) :
Bool

Returns true if the given declaration has a `@[csimp]` lemma.

Equations

- Mathlib.Util.hasCSimpLemma env n = (Lean.ScopedEnvExtension.getState Lean.Compiler.CSimp.ext env).map.contains n

Instances For

source
def Mathlib.Util.«commandCompile_def%_» :
Lean.ParserDescr

`compile_def% Foo.foo` adds compiled code for the definition `Foo.foo`. This can be used for type class projections or definitions like `List._sizeOf_1`, for which Lean does not generate compiled code by default (since it is not used 99% of the time).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Util.compileInductiveOnly (iv : Lean.InductiveVal) (rv : Lean.RecursorVal) (warn : Bool := true) :
Lean.MetaM Unit

Generate compiled code for the recursor for `iv`, excluding the `sizeOf` function.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Mathlib.Util.compileInductive (iv : Lean.InductiveVal) (warn : Bool := true) :
Lean.MetaM Unit

Generate compiled code for the recursor for `iv`.

source
partial def Mathlib.Util.compileSizeOf (iv : Lean.InductiveVal) (rv : Lean.RecursorVal) :
Lean.MetaM Unit

Compiles the `sizeOf` auxiliary functions. It also recursively compiles any inductives required to compile the `sizeOf` definition (because `sizeOf` definitions depend on `T.rec`).

source
def Mathlib.Util.«commandCompile_inductive%_» :
Lean.ParserDescr

`compile_inductive% Foo` creates compiled code for the recursor `Foo.rec`, so that `Foo.rec` can be used in a definition without having to mark the definition as `noncomputable`.

Equations

- One or more equations did not get rendered due to their size.

Instances For