Trait ExFuture 

pub trait ExFuture {
    type ExternalTraitSpecificationFor: Future;
    type Output;

    // Required methods
    spec fn obeys_future_laws(&self) -> bool;
    spec fn view(&self) -> Self::Output;
    exec fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> r : Poll<Self::Output>;
}

Required Associated Types

type ExternalTraitSpecificationFor: Future

type Output

Required Methods

spec fn obeys_future_laws(&self) -> bool

Whether this future obeys the specification below on poll, so that awaiting it returns view().

spec fn view(&self) -> Self::Output

The value that awaiting this future will return.

exec fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> r : Poll<Self::Output>

ensures

({
    let m = self.mut_ref();
    &&& m.future.value().obeys_future_laws() == m.current.obeys_future_laws()
    &&& m.current.obeys_future_laws()
        ==> match r {
            Poll::Ready(v) => v == m.current.view(),
            Poll::Pending => m.future.value().view() == m.current.view(),
        }

}),

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors