Trait ContainsSpec 

pub trait ContainsSpec<Idx, U>
where
    Idx: PartialOrd<U>,
    U: ?Sized + PartialOrd<Idx>,
{
    // Required methods
    spec fn obeys_contains() -> bool;
    spec fn contains_spec(&self, i: &U) -> bool;
}

Required Methods

spec fn obeys_contains() -> bool

spec fn contains_spec(&self, i: &U) -> bool

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl<Idx, U> ContainsSpec<Idx, U> for Range<Idx>

where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>,

open spec fn obeys_contains() -> bool

{ (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec()) }

open spec fn contains_spec(&self, i: &U) -> bool

{ self.start.is_le(&i) && i.is_lt(&self.end) }

impl<Idx, U> ContainsSpec<Idx, U> for RangeInclusive<Idx>

where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>,

open spec fn obeys_contains() -> bool

{ (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec()) }

open spec fn contains_spec(&self, i: &U) -> bool

{
    self@.start.is_le(&i)
        && if self@.exhausted { i.is_lt(&self@.end) } else { i.is_le(&self@.end) }
}

Implementors