Module lean_sys::init

Utilities for initializing Lean’s runtime

Statics

• LEAN_INIT_MUTEX
  A convenience mutex, since lean_initialize_runtime_module and lean_initialize are not thread-safe.

Functions

• lean_initialize^⚠
• lean_initialize_locked^⚠
  A helper function to call lean_initialize while holding the LEAN_INIT_MUTEX./// This is equivalent to writing
• lean_initialize_runtime_module^⚠
• lean_initialize_runtime_module_locked^⚠
  A helper function to call lean_initialize_runtime_module while holding the LEAN_INIT_MUTEX.