- adhoc (backend : Name) : ExternEntry
- inline (backend : Name) (pattern : String) : ExternEntry
- standard (backend : Name) (fn : String) : ExternEntry
- foreign (backend : Name) (fn : String) : ExternEntry
Instances For
@[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"]
- entries : List ExternEntry
Instances For
@[extern lean_add_extern]
@[export lean_get_extern_attr_data]
Equations
Instances For
Equations
Instances For
Equations
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
Instances For
@[export lean_get_extern_const_arity]