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

Equations

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

@[inline]

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

Equations

• Lean.registerInitAttr attrName runAfterImport ref = Lean.registerInitAttrInner✝ attrName runAfterImport ref

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

Equations

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

@[export lean_get_builtin_init_fn_name_for]

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

Equations

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

@[export lean_get_regular_init_fn_name_for]

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

Equations

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

@[export lean_get_init_fn_name_for]

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

Equations

• Lean.getInitFnNameFor? env fn = (Lean.getBuiltinInitFnNameFor? env fn <|> Lean.getRegularInitFnNameFor? env fn)

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

Equations

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

@[export lean_is_io_unit_regular_init_fn]

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

Equations

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

@[export lean_is_io_unit_builtin_init_fn]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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