Skip to main content

PartialEqSpecImpl

vstd::std_specs::cmp

Trait PartialEqSpecImpl 

Source 
pub trait PartialEqSpecImpl<Rhs: PointeeSized = Self>: PointeeSized + PartialEq<Rhs> {
    // Required methods
    exec fn obeys_eq_spec() -> bool;
    exec fn eq_spec(&self, other: &Rhs) -> bool;
}

Required Methods§

Source

exec fn obeys_eq_spec() -> bool

Source

exec fn eq_spec(&self, other: &Rhs) -> 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 PartialEqSpecImpl for bool

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &bool) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for i8

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &i8) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for i16

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &i16) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for i32

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &i32) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for i64

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &i64) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for i128

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &i128) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for isize

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &isize) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for u8

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &u8) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for u16

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &u16) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for u32

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &u32) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for u64

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &u64) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for u128

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &u128) -> bool

{ *self == *other }
Source§

impl PartialEqSpecImpl for usize

Source§

open spec fn obeys_eq_spec() -> bool

{ true }
Source§

open spec fn eq_spec(&self, other: &usize) -> bool

{ *self == *other }
Source§

impl<A, B: PointeeSized> PartialEqSpecImpl<&B> for &A
where A: PartialEq<B> + PointeeSized,

Source§

open spec fn obeys_eq_spec() -> bool

{ <A as PartialEqSpec<B>>::obeys_eq_spec() }
Source§

open spec fn eq_spec(&self, other: &&B) -> bool

{ <A as PartialEqSpec<B>>::eq_spec(*self, *other) }
Source§

impl<A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (A, Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& A::eq_spec(&self.0, &other.0)
    &&& Z::eq_spec(&self.1, &other.1)
    &&& Y::eq_spec(&self.2, &other.2)
    &&& X::eq_spec(&self.3, &other.3)
    &&& W::eq_spec(&self.4, &other.4)
    &&& V::eq_spec(&self.5, &other.5)
    &&& U::eq_spec(&self.6, &other.6)
    &&& T::eq_spec(&self.7, &other.7)

}
Source§

impl<B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (B, A, Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& B::eq_spec(&self.0, &other.0)
    &&& A::eq_spec(&self.1, &other.1)
    &&& Z::eq_spec(&self.2, &other.2)
    &&& Y::eq_spec(&self.3, &other.3)
    &&& X::eq_spec(&self.4, &other.4)
    &&& W::eq_spec(&self.5, &other.5)
    &&& V::eq_spec(&self.6, &other.6)
    &&& U::eq_spec(&self.7, &other.7)
    &&& T::eq_spec(&self.8, &other.8)

}
Source§

impl<C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (C, B, A, Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& C::eq_spec(&self.0, &other.0)
    &&& B::eq_spec(&self.1, &other.1)
    &&& A::eq_spec(&self.2, &other.2)
    &&& Z::eq_spec(&self.3, &other.3)
    &&& Y::eq_spec(&self.4, &other.4)
    &&& X::eq_spec(&self.5, &other.5)
    &&& W::eq_spec(&self.6, &other.6)
    &&& V::eq_spec(&self.7, &other.7)
    &&& U::eq_spec(&self.8, &other.8)
    &&& T::eq_spec(&self.9, &other.9)

}
Source§

impl<D: PartialEq + PartialEqSpec, C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (D, C, B, A, Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& D::obeys_eq_spec()
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(D, C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& D::eq_spec(&self.0, &other.0)
    &&& C::eq_spec(&self.1, &other.1)
    &&& B::eq_spec(&self.2, &other.2)
    &&& A::eq_spec(&self.3, &other.3)
    &&& Z::eq_spec(&self.4, &other.4)
    &&& Y::eq_spec(&self.5, &other.5)
    &&& X::eq_spec(&self.6, &other.6)
    &&& W::eq_spec(&self.7, &other.7)
    &&& V::eq_spec(&self.8, &other.8)
    &&& U::eq_spec(&self.9, &other.9)
    &&& T::eq_spec(&self.10, &other.10)

}
Source§

impl<E: PartialEq + PartialEqSpec, D: PartialEq + PartialEqSpec, C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (E, D, C, B, A, Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& E::obeys_eq_spec()
    &&& D::obeys_eq_spec()
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(E, D, C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& E::eq_spec(&self.0, &other.0)
    &&& D::eq_spec(&self.1, &other.1)
    &&& C::eq_spec(&self.2, &other.2)
    &&& B::eq_spec(&self.3, &other.3)
    &&& A::eq_spec(&self.4, &other.4)
    &&& Z::eq_spec(&self.5, &other.5)
    &&& Y::eq_spec(&self.6, &other.6)
    &&& X::eq_spec(&self.7, &other.7)
    &&& W::eq_spec(&self.8, &other.8)
    &&& V::eq_spec(&self.9, &other.9)
    &&& U::eq_spec(&self.10, &other.10)
    &&& T::eq_spec(&self.11, &other.11)

}
Source§

impl<T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (T,)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(T,)) -> bool

{
    &&& T::eq_spec(&self.0, &other.0)

}
Source§

impl<T: PartialEqSpec> PartialEqSpecImpl for Option<T>

Source§

open spec fn obeys_eq_spec() -> bool

{ T::obeys_eq_spec() }
Source§

open spec fn eq_spec(&self, other: &Option<T>) -> bool

{
    match (self, other) {
        (None, None) => true,
        (Some(x), Some(y)) => x.eq_spec(y),
        _ => false,
    }
}
Source§

impl<T: PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1>

Source§

open spec fn obeys_eq_spec() -> bool

{ T::obeys_eq_spec() }
Source§

open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool

{
    &&& self.len() == other.len()
    &&& forall |i: int| 0 <= i < self.len() ==> self[i].eq_spec(&other[i])

}
Source§

impl<U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(U, T)) -> bool

{
    &&& U::eq_spec(&self.0, &other.0)
    &&& T::eq_spec(&self.1, &other.1)

}
Source§

impl<V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(V, U, T)) -> bool

{
    &&& V::eq_spec(&self.0, &other.0)
    &&& U::eq_spec(&self.1, &other.1)
    &&& T::eq_spec(&self.2, &other.2)

}
Source§

impl<W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(W, V, U, T)) -> bool

{
    &&& W::eq_spec(&self.0, &other.0)
    &&& V::eq_spec(&self.1, &other.1)
    &&& U::eq_spec(&self.2, &other.2)
    &&& T::eq_spec(&self.3, &other.3)

}
Source§

impl<X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(X, W, V, U, T)) -> bool

{
    &&& X::eq_spec(&self.0, &other.0)
    &&& W::eq_spec(&self.1, &other.1)
    &&& V::eq_spec(&self.2, &other.2)
    &&& U::eq_spec(&self.3, &other.3)
    &&& T::eq_spec(&self.4, &other.4)

}
Source§

impl<Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(Y, X, W, V, U, T)) -> bool

{
    &&& Y::eq_spec(&self.0, &other.0)
    &&& X::eq_spec(&self.1, &other.1)
    &&& W::eq_spec(&self.2, &other.2)
    &&& V::eq_spec(&self.3, &other.3)
    &&& U::eq_spec(&self.4, &other.4)
    &&& T::eq_spec(&self.5, &other.5)

}
Source§

impl<Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (Z, Y, X, W, V, U, T)

Source§

open spec fn obeys_eq_spec() -> bool

{
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}
Source§

open spec fn eq_spec(&self, other: &(Z, Y, X, W, V, U, T)) -> bool

{
    &&& Z::eq_spec(&self.0, &other.0)
    &&& Y::eq_spec(&self.1, &other.1)
    &&& X::eq_spec(&self.2, &other.2)
    &&& W::eq_spec(&self.3, &other.3)
    &&& V::eq_spec(&self.4, &other.4)
    &&& U::eq_spec(&self.5, &other.5)
    &&& T::eq_spec(&self.6, &other.6)

}

Implementors§