Documentation

Lean.Compiler.InitAttr

@[extern lean_run_mod_init]
unsafe opaque Lean.runModInit (mod : Lake.Name) :

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 : Lean.Environment) (opts : Lean.Options) (decl : Lake.Name) (initDecl : Lake.Name) :

Run the initializer for decl and store its value for global access. Should only be used while importing.

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

unsafe def Lean.registerInitAttrUnsafe (attrName : Lake.Name) (runAfterImport : Bool) (ref : Lake.Name) :
Instances For
    @[inline]
    Equations
    Instances For
      Equations
      Instances For
        @[export lean_get_builtin_init_fn_name_for]
        Equations
        Instances For
          @[export lean_get_regular_init_fn_name_for]
          Equations
          Instances For
            @[export lean_get_init_fn_name_for]
            Equations
            Instances For
              Equations
              Instances For
                @[export lean_is_io_unit_regular_init_fn]
                Equations
                Instances For
                  @[export lean_is_io_unit_builtin_init_fn]
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For