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.

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.

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.

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

Returns true if the given declaration has already been compiled, either directly or via a @[csimp] lemma.

Equations

• Mathlib.Util.isCompiled env n = (Lean.SMap.contains env.toKernelEnv.constants (n.str "_cstage2") || (Lean.ScopedEnvExtension.getState Lean.Compiler.CSimp.ext env).map.contains n)

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.

def Mathlib.Util.compileInductiveOnly (iv : Lean.InductiveVal) (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.

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

Generate compiled code for the recursor for iv.

partial def Mathlib.Util.compileSizeOf (iv : Lean.InductiveVal) : 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).

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.