compile_inductive% command. #
compile_inductive% Foo adds compiled code for the recursor
working around a bug in the core Lean compiler which does not support recursors.
For technical reasons, the recursor code generated by
unfortunately evaluates the base cases eagerly. That is,
List.rec (unreachable!) (fun _ _ _ => 42)  will panic.
compile_def% Foo.foo adds compiled code for definitions when missing.
This can be the case for type class projections, or definitions like
compile_def% Foo.foo adds compiled code for the definition
This can be used for type class projections or definitions like
for which Lean does not generate compiled code by default
(since it is not used 99% of the time).