inductive Lean.ExternEntry : Type

• adhoc (backend : Name) : ExternEntry
• inline (backend : Name) (pattern : String) : ExternEntry
• standard (backend : Name) (fn : String) : ExternEntry
• opaque (fn : Name) : ExternEntry

  Call to a Lean function without exported IR.

instance Lean.instBEqExternEntry : BEq ExternEntry

instance Lean.instHashableExternEntry : Hashable ExternEntry

structure Lean.ExternAttrData : Type

• @[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"]

• arity? : Option Nat
• entries : List ExternEntry

instance Lean.instInhabitedExternAttrData : Inhabited ExternAttrData

instance Lean.instBEqExternAttrData : BEq ExternAttrData

instance Lean.instHashableExternAttrData : Hashable ExternAttrData

@[extern lean_add_extern]

opaque Lean.addExtern (env : Environment) (n : Name) : ExceptT String Id Environment

opaque Lean.externAttr : ParametricAttribute ExternAttrData

@[export lean_get_extern_attr_data]

def Lean.getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData

def Lean.expandExternPatternAux (args : List String) : Nat → String.Iterator → String → String

def Lean.expandExternPattern (pattern : String) (args : List String) : String

def Lean.mkSimpleFnCall (fn : String) (args : List String) : String

def Lean.ExternEntry.backend : ExternEntry → Name

def Lean.getExternEntryForAux (backend : Name) : List ExternEntry → Option ExternEntry

def Lean.getExternEntryFor (d : ExternAttrData) (backend : Name) : Option ExternEntry

def Lean.isExtern (env : Environment) (fn : Name) : Bool

def Lean.isExternC (env : Environment) (fn : Name) : Bool

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.

def Lean.getExternNameFor (env : Environment) (backend fn : Name) : Option String

@[export lean_get_extern_const_arity]

def Lean.getExternConstArityExport (env : Environment) (declName : Name) : IO (Option Nat)