inductive Lean.ExternEntry : Type

• adhoc: Lake.Name → Lean.ExternEntry
• inline: Lake.Name → String → Lean.ExternEntry
• standard: Lake.Name → String → Lean.ExternEntry
• foreign: Lake.Name → String → Lean.ExternEntry

structure Lean.ExternAttrData : Type

• arity? : Option Nat
• 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"]

instance Lean.instInhabitedExternAttrData : Inhabited Lean.ExternAttrData

@[extern lean_add_extern]

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

opaque Lean.externAttr : Lean.ParametricAttribute Lean.ExternAttrData

@[export lean_get_extern_attr_data]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.expandExternPatternAux args 0 x x = x

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

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

def Lean.ExternEntry.backend : Lean.ExternEntry → Lake.Name

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.getExternEntryForAux backend [] = none

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

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

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

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.

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

@[export lean_get_extern_const_arity]

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