Lean.Compiler.InitAttr

@[extern lean_run_mod_init]

unsafe opaque Lean.runModInit (mod : Lean.Name) :

Run the initializer of the given module (without builtin_initialize commands). Return false if the initializer is not available as native code. Initializers do not have corresponding Lean definitions, so they cannot be interpreted in this case.

source

@[extern lean_run_init]

unsafe opaque Lean.runInit (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Name) (initDecl : Lean.Name) :

IO Unit

Run the initializer for decl and store its value for global access. Should only be used while importing.

source

unsafe def Lean.registerInitAttrUnsafe (attrName : Lean.Name) (runAfterImport : Bool) :

IO (Lean.ParametricAttribute Lean.Name)

Equations

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

source

@[implementedBy Lean.registerInitAttrUnsafe]

opaque Lean.registerInitAttr (attrName : Lean.Name) (runAfterImport : Bool) :

IO (Lean.ParametricAttribute Lean.Name)

source

opaque Lean.regularInitAttr:

Lean.ParametricAttribute Lean.Name

source

opaque Lean.builtinInitAttr:

Lean.ParametricAttribute Lean.Name

source

def Lean.getInitFnNameForCore? (env : Lean.Environment) (attr : Lean.ParametricAttribute Lean.Name) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getInitFnNameForCore? env attr fn = match Lean.ParametricAttribute.getParam attr env fn with | some Lean.Name.anonymous => none | some n => some n | x => none

source

@[export lean_get_builtin_init_fn_name_for]

def Lean.getBuiltinInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getBuiltinInitFnNameFor? env fn = Lean.getInitFnNameForCore? env Lean.builtinInitAttr fn

source

@[export lean_get_regular_init_fn_name_for]

def Lean.getRegularInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getRegularInitFnNameFor? env fn = Lean.getInitFnNameForCore? env Lean.regularInitAttr fn

source

@[export lean_get_init_fn_name_for]

def Lean.getInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getInitFnNameFor? env fn = HOrElse.hOrElse (Lean.getBuiltinInitFnNameFor? env fn) fun x => Lean.getRegularInitFnNameFor? env fn

source

def Lean.isIOUnitInitFnCore (env : Lean.Environment) (attr : Lean.ParametricAttribute Lean.Name) (fn : Lean.Name) :

Bool

Equations

Lean.isIOUnitInitFnCore env attr fn = match Lean.ParametricAttribute.getParam attr env fn with | some Lean.Name.anonymous => true | x => false

source

@[export lean_is_io_unit_regular_init_fn]

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

Bool

Equations

Lean.isIOUnitRegularInitFn env fn = Lean.isIOUnitInitFnCore env Lean.regularInitAttr fn

source

@[export lean_is_io_unit_builtin_init_fn]

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

Bool

Equations

Lean.isIOUnitBuiltinInitFn env fn = Lean.isIOUnitInitFnCore env Lean.builtinInitAttr fn

source

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

Bool

Equations

Lean.isIOUnitInitFn env fn = (Lean.isIOUnitBuiltinInitFn env fn || Lean.isIOUnitRegularInitFn env fn)

source

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

Bool

Equations

Lean.hasInitAttr env fn = Option.isSome (Lean.getInitFnNameFor? env fn)

source

def Lean.setBuiltinInitAttr (env : Lean.Environment) (declName : Lean.Name) (initFnName : optParam Lean.Name Lean.Name.anonymous) :

Except String Lean.Environment

Equations

Lean.setBuiltinInitAttr env declName initFnName = Lean.ParametricAttribute.setParam Lean.builtinInitAttr env declName initFnName

source

def Lean.declareBuiltin (forDecl : Lean.Name) (value : Lean.Expr) :

Lean.CoreM Unit

Equations

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