Helper functions for creating auxiliary names used in (old) compiler passes.
@[export lean_mk_eager_lambda_lifting_name]
Equations
Instances For
@[export lean_is_eager_lambda_lifting_name]
Equations
Instances For
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
Instances For
Equations
Instances For
@[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
Instances For
@[export lean_is_unsafe_rec_name]
Return some _
if the given name was created using mkUnsafeRecName