Documentation

Mathlib.Util.CompileInductive

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.

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

Equations
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For

              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
                Instances For

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

                  Equations
                    Instances For

                      Generate compiled code for the recursor for iv.

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

                      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
                        Instances For