ContainsSpec

vstd::std_specs::range

Trait ContainsSpec 

Source 
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§

Source

spec fn obeys_contains() -> bool

Source

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", so this trait is not object safe.

Implementations on Foreign Types§

Source§

impl<Idx, U> ContainsSpec<Idx, U> for Range<Idx>
where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>,

Source§

open spec fn obeys_contains() -> bool

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

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

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

impl<Idx, U> ContainsSpec<Idx, U> for RangeInclusive<Idx>
where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>,

Source§

open spec fn obeys_contains() -> bool

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

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§