Trait FutureSpec 

pub trait FutureSpec: Future {
    // Required methods
    spec fn obeys_future_laws(&self) -> bool;
    spec fn view(&self) -> Self::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.

Dyn Compatibility

This trait is dyn compatible.

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

Implementors

impl<VERUS_SPEC__A: Future + ?Sized> FutureSpec for VERUS_SPEC__A