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
    @[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.

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