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
    @[extern lean_add_extern]
    @[export lean_get_extern_attr_data]
    Instances For
      Equations
      Instances For
        Instances For
          Instances For
            Equations
            Instances For
              Instances For

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

                Instances For
                  Instances For
                    @[export lean_get_extern_const_arity]
                    Instances For