Struct LeanIo 

pub struct LeanIo<T>(/* private fields */);

Return-type marker for Lean exports declared IO α.

Writing exported::<Args, LeanIo<T>>(name) makes LeanExported’s .call method compose decode_io before TryFromLean::try_from_lean, so the handle returns LeanResult<T>. The marker has no value — it is a pure type-level switch.

LeanIo<T> cannot be constructed from outside the crate (its single field is private); it appears only in R positions on LeanModule::exported.

Trait Implementations

impl<'lean, T> DecodeCallResult<'lean> for LeanIo<T>

where T: TryFromLean<'lean>,

type Output = T

What .call(...) returns inside LeanResult.

type CRepr = *mut lean_object

The C-ABI return type of the Lake-emitted function. For the pure path this is T::CRepr (e.g. u8 for Bool exports, *mut lean_object for String); for the IO path it is always *mut lean_object (the lean_io_result_* wrapper).