- adhoc: Lake.Name → Lean.ExternEntry
- inline: Lake.Name → String → Lean.ExternEntry
- standard: Lake.Name → String → Lean.ExternEntry
- foreign: Lake.Name → String → Lean.ExternEntry
Instances For
- entries : List Lean.ExternEntry
@[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
- One or more equations did not get rendered due to their size.
- Lean.expandExternPatternAux args 0 x x = x
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.getExternEntryForAux backend [] = none
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]