pub unsafe extern "C" fn lean_initialize()Expand description
Initialize the Lean runtime. Must be called exactly once per process before any other Lean-runtime entry point. The C signature in the runtime accepts no arguments.
pub unsafe extern "C" fn lean_initialize()Initialize the Lean runtime. Must be called exactly once per process before any other Lean-runtime entry point. The C signature in the runtime accepts no arguments.