@[extern lean_run_mod_init]

unsafe opaque Lean.runModInit (mod : Lake.Name) : IO Bool

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.

@[extern lean_run_init]

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

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

opaque Lean.interpretedModInits : IO.Ref Lean.NameSet

Set of modules for which we have already run the module initializer in the interpreter.

unsafe def Lean.registerInitAttrUnsafe (attrName : Lake.Name) (runAfterImport : Bool) (ref : Lake.Name) : IO (Lean.ParametricAttribute Lake.Name)

@[inline]

def Lean.registerInitAttr (attrName : Lake.Name) (runAfterImport : Bool) (ref : autoParam Lake.Name _auto✝) : IO (Lean.ParametricAttribute Lake.Name)

opaque Lean.regularInitAttr : Lean.ParametricAttribute Lake.Name

opaque Lean.builtinInitAttr : Lean.ParametricAttribute Lake.Name

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

@[export lean_get_builtin_init_fn_name_for]

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

@[export lean_get_regular_init_fn_name_for]

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

@[export lean_get_init_fn_name_for]

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

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

@[export lean_is_io_unit_regular_init_fn]

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

@[export lean_is_io_unit_builtin_init_fn]

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

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

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

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

def Lean.declareBuiltin (forDecl : Lake.Name) (value : Lean.Expr) : Lean.CoreM Unit