# Documentation

Lean.Compiler.Old

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

@[export lean_mk_eager_lambda_lifting_name]
Equations
@[export lean_is_eager_lambda_lifting_name]

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
• One or more equations did not get rendered due to their size.
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
@[extern lean_compile_decls]
opaque Lean.Environment.compileDecls (env : Lean.Environment) (opt : Lean.Options) (decls : ) :

Compile the given block of mutual declarations. Assumes the declarations have already been added to the environment using addDecl.

Compile the given declaration, it assumes the declaration has already been added to the environment using addDecl.

Equations