Documentation

Lean.Compiler.ExternAttr

  • @[extern] encoding: .entries = [adhoc `all]
  • @[extern "level_hash"] encoding: .entries = [standard `all "levelHash"]
  • @[extern cpp "lean::string_size" llvm "lean_str_size"] encoding: .entries = [standard `cpp "lean::string_size", standard `llvm "leanStrSize"]
  • @[extern cpp inline "#1 + #2"] encoding: .entries = [inline `cpp "#1 + #2"]
  • @[extern cpp "foo" llvm adhoc] encoding: .entries = [standard `cpp "foo", adhoc `llvm]
  • @[extern 2 cpp "io_prim_println"] encoding: .arity? = 2, .entries = [standard `cpp "ioPrimPrintln"]
Instances For
    Equations
    @[extern lean_add_extern]
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For

              We say a Lean function marked as [extern "<c_fn_nane>"] is for all backends, and it is implemented using extern "C". Thus, there is no name mangling.

              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[export lean_get_extern_const_arity]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For