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

• @[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 Lean.ExternEntry

instance Lean.instInhabitedExternAttrData : Inhabited Lean.ExternAttrData

Equations

• Lean.instInhabitedExternAttrData = { default := { arity? := default, entries := default } }

@[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

Equations

• Lean.getExternAttrData? env n = Lean.externAttr.getParam? env n

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

Equations

• Lean.expandExternPattern pattern args = Lean.expandExternPatternAux args pattern.length pattern.mkIterator ""

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

Equations

• Lean.mkSimpleFnCall fn args = fn ++ "(" ++ List.foldl (fun (x1 x2 : String) => x1 ++ x2) "" (List.intersperse ", " args) ++ ")"

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

Equations

• (Lean.ExternEntry.adhoc n).backend = n
• (Lean.ExternEntry.inline n pattern).backend = n
• (Lean.ExternEntry.standard n fn).backend = n
• (Lean.ExternEntry.foreign n fn).backend = n

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

Equations

• Lean.getExternEntryForAux backend [] = none
• Lean.getExternEntryForAux backend (e :: es) = if (e.backend == `all) = true then some e else if (e.backend == backend) = true then some e else Lean.getExternEntryForAux backend es

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

Equations

• Lean.getExternEntryFor d backend = Lean.getExternEntryForAux backend d.entries

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

Equations

• Lean.isExtern env fn = (Lean.getExternAttrData? env fn).isSome

def Lean.isExternC (env : Lean.Environment) (fn : Lake.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.

Equations

• Lean.isExternC env fn = match Lean.getExternAttrData? env fn with | some { arity? := arity?, entries := [Lean.ExternEntry.standard `all fn] } => true | x => false

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

Equations

• One or more equations did not get rendered due to their size.

@[export lean_get_extern_const_arity]

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

Equations

• One or more equations did not get rendered due to their size.