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

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

source
opaque Lean.interpretedModInits :
IO.Ref NameSet

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

source
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.

Instances For

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

Instances For

source
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.

source
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.

source
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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For