Documentation

Lean.Compiler.Old

Helper functions for creating auxiliary names used in (old) compiler passes.

@[export lean_mk_eager_lambda_lifting_name]
Equations

Return the name of new definitions in the a given declaration. Here we consider only declarations we generate code for. We use this definition to implement add_and_compile.

Equations
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_mk_unsafe_rec_name]

We generate auxiliary unsafe definitions for regular recursive definitions. The auxiliary unsafe definition has a clear runtime cost execution model. This function returns the auxiliary unsafe definition name for the given name.

Equations
@[export lean_is_unsafe_rec_name]

Return some _ if the given name was created using mkUnsafeRecName

Equations