Documentation

Lean.Compiler.InitAttr

@[extern lean_run_mod_init]
unsafe opaque Lean.runModInit (mod : 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 : Environment) (opts : Options) (decl initDecl : 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 : Name) (runAfterImport : Bool) (ref : Name) :
Equations
    Instances For
      @[inline]
      def Lean.registerInitAttr (attrName : Name) (runAfterImport : Bool) (ref : Name := by exact decl_name%) :
      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
                                                Instances For
                                                  def Lean.declareBuiltin (forDecl : Name) (value : Expr) :
                                                  Equations
                                                    Instances For