Expand description
Utilities for initializing Lean’s runtime
Statics
A convenience mutex, since
lean_initialize_runtime_module
and lean_initialize
are not thread-safe.Functions
A helper function to call
lean_initialize
while holding the LEAN_INIT_MUTEX
.///
This is equivalent to writingA helper function to call
lean_initialize_runtime_module
while holding the LEAN_INIT_MUTEX
.