Documentation

Lean.Compiler.Old

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

@[export lean_mk_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
      • One or more equations did not get rendered due to their size.
      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

          Equations
          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.

            Equations
            Instances For