Documentation

Lean.Compiler.ExternAttr

inductive Lean.ExternEntry:

Type

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

structure Lean.ExternAttrData:

Type

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 : Lean.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 : Lean.Name) :

Option Lean.ExternAttrData

Equations

Lean.getExternAttrData env n = Lean.ParametricAttribute.getParam Lean.externAttr 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 _fun_discr _fun_discr = _fun_discr

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

Equations

Lean.expandExternPattern pattern args = Lean.expandExternPatternAux args (String.length pattern) (String.mkIterator pattern) ""

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

Equations

Lean.mkSimpleFnCall fn args = fn ++ "(" ++ List.foldl (fun a a_1 => a ++ a_1) "" (List.intersperse ", " args) ++ ")"

def Lean.ExternEntry.backend:

Lean.ExternEntry → Lean.Name

Equations

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

def Lean.getExternEntryForAux (backend : Lean.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 : Lean.Name) :

Option Lean.ExternEntry

Equations

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

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

Equations

Lean.isExtern env fn = Option.isSome (Lean.getExternAttrData env fn)

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

Equations

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

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

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 : Lean.Name) :

IO (Option Nat)

Equations

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