Trait DecodeCallResult 

pub trait DecodeCallResult<'lean>: Sized + SealedResult {
    type Output;
    type CRepr: Copy;
}

How to decode an owned Lean call result into a Rust value.

Sealed via SealedResult; downstream cannot implement it. Two implementors:

• blanket impl<T: LeanAbi<'lean>> DecodeCallResult<'lean> for T — the pure path; CRepr = T::CRepr, Output = T; decode_c is T::from_c(c, rt).
• special impl<T: TryFromLean<'lean>> DecodeCallResult<'lean> for LeanIo<T> — the IO path; CRepr = *mut lean_object (the IO result wrapper), Output = T; decode_c wraps the pointer in Obj, runs decode_io, then T::try_from_lean.

Coherence holds because LeanIo<T> does not implement LeanAbi, so the blanket impl does not match it.

Required Associated Types

type Output

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

type CRepr: Copy

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).

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

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

where T: TryFromLean<'lean>,

type Output = T

type CRepr = *mut lean_object

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

where T: LeanAbi<'lean>,

type Output = T

type CRepr = <T as LeanAbi<'lean>>::CRepr