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

opaque Lean.builtinInitAttr : ParametricAttribute Name

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.