Documentation

Lean.Compiler.Old

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

@[export lean_mk_eager_lambda_lifting_name]
Instances For
    @[export lean_is_eager_lambda_lifting_name]
    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.

      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.

        Instances For
          @[export lean_is_unsafe_rec_name]

          Return some _ if the given name was created using mkUnsafeRecName

          Instances For
            @[extern lean_compile_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.

            Instances For