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

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

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

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