pub unsafe extern "C" fn lean_initialize_runtime_module()Expand description
Initialize the runtime module (compact regions, persistent objects).
Must be called after lean_initialize and before invoking any
compiled Lean module’s init entry point.