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