lean_initialize_runtime_module_locked

Function lean_initialize_runtime_module_locked 

Source
pub unsafe fn lean_initialize_runtime_module_locked()
Expand description

A helper function to call lean_initialize_runtime_module while holding the LEAN_INIT_MUTEX.

This is equivalent to writing

unsafe {
    let guard = LEAN_INIT_MUTEX.lock();
    lean_initialize_runtime_module();
}