inductive Lean.ExternEntry : Type

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

instance Lean.instBEqExternEntry : BEq ExternEntry

Equations

• Lean.instBEqExternEntry = { beq := Lean.beqExternEntry✝ }

instance Lean.instHashableExternEntry : Hashable ExternEntry

Equations

• Lean.instHashableExternEntry = { hash := Lean.hashExternEntry✝ }

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

Equations

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

instance Lean.instBEqExternAttrData : BEq ExternAttrData

Equations

• Lean.instBEqExternAttrData = { beq := Lean.beqExternAttrData✝ }

instance Lean.instHashableExternAttrData : Hashable ExternAttrData

Equations

• Lean.instHashableExternAttrData = { hash := Lean.hashExternAttrData✝ }

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

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 : ExternEntry → Name

Equations

• (Lean.ExternEntry.adhoc a).backend = a
• (Lean.ExternEntry.inline a a_1).backend = a
• (Lean.ExternEntry.standard a a_1).backend = a
• (Lean.ExternEntry.foreign a a_1).backend = a

def Lean.getExternEntryForAux (backend : Name) : List ExternEntry → Option 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 : ExternAttrData) (backend : Name) : Option ExternEntry

Equations

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

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

Equations

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

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.

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 : Environment) (backend fn : 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 : Environment) (declName : Name) : IO (Option Nat)

Equations

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