@[extern lean_run_mod_init]

unsafe opaque Lean.runModInit (mod : 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 : Environment) (opts : Options) (decl initDecl : 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 NameSet

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

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

@[inline]

def Lean.registerInitAttr (attrName : Name) (runAfterImport : Bool) (ref : Name := by exact decl_name%) : IO (ParametricAttribute Name)

opaque Lean.regularInitAttr : ParametricAttribute Name

Registers an initialization procedure. Initialization procedures are run in files that import the file they are defined in.

This attribute comes in two kinds: Without arguments, the tagged declaration should have type IO Unit and are simply run during initialization. With a declaration name as a argument, the tagged declaration should be an opaque constant and the provided declaration name an action in IO that returns a value of the type of the tagged declaration. Such initialization procedures store the resulting value and make it accessible through the tagged declaration.

The initialize command should usually be preferred over using this attribute directly.

opaque Lean.builtinInitAttr : ParametricAttribute Name

Registers a builtin initialization procedure.

This attribute is used internally to define builtin initialization procedures for bootstrapping and should not be used otherwise.

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

@[export lean_get_builtin_init_fn_name_for]

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

@[export lean_get_regular_init_fn_name_for]

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

@[export lean_get_init_fn_name_for]

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

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

@[export lean_is_io_unit_regular_init_fn]

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

@[export lean_is_io_unit_builtin_init_fn]

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

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

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

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

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