Module io 

IO-result helpers — mirrors lean.h:2893–2907.

IO α results from compiled Lean are encoded as constructors with tag 0 (ok) or tag 1 (error). The single object payload sits in constructor slot 0; reading it requires the ctor accessors implemented against LeanCtorObjectRepr.

Functions

lean_io_mark_end_initialization^⚠

Signal that runtime initialization is complete; subsequent allocations should not flag objects as persistent (lean.h:2907).

lean_io_result_get_error^⚠

Borrow the error out of an IO.error result (lean.h:2896).

lean_io_result_get_value^⚠

Borrow the value out of an IO.ok result (lean.h:2895).

lean_io_result_is_error^⚠

True if r is an IO.error result (lean.h:2894).

lean_io_result_is_ok^⚠

True if r is an IO.ok result (lean.h:2893).

lean_io_result_take_value^⚠

Take ownership of the value out of an IO.ok result (lean.h:2898–2903).