inductive Lean.ExternEntry : Type

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

  Call to a Lean function without exported IR.

def Lean.instBEqExternEntry.beq : ExternEntry → ExternEntry → Bool

instance Lean.instBEqExternEntry : BEq ExternEntry

def Lean.instHashableExternEntry.hash : ExternEntry → UInt64

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]

• entries : List ExternEntry

def Lean.instInhabitedExternAttrData.default : ExternAttrData

instance Lean.instInhabitedExternAttrData : Inhabited ExternAttrData

def Lean.instBEqExternAttrData.beq : ExternAttrData → ExternAttrData → Bool

instance Lean.instBEqExternAttrData : BEq ExternAttrData

instance Lean.instHashableExternAttrData : Hashable ExternAttrData

def Lean.instHashableExternAttrData.hash : ExternAttrData → UInt64

@[extern lean_add_extern]

opaque Lean.addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit

opaque Lean.externAttr : ParametricAttribute ExternAttrData

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

def Lean.expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.Pos) → 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) (entries : 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_name>"] 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