Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126use super::super::prelude::*;
verus! {
// array == arraypub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<[U; N]>>::eq ]( left: &[T; N], right: &[U; N],) -> bool;
impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for [T; N] where T: PartialEq<U> + super::cmp::PartialEqSpec<U>, { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &[U; N]) -> bool { forall|i: int| #![auto] 0 <= i < N ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i]) }}
// slice ref == arraypub assume_specification<'a, T: PartialEq<U>, U, const N: usize>[ <&'a [T] as PartialEq< [U; N],>>::eq ](left: &&'a [T], right: &[U; N]) -> bool;
impl<'a, T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for &'a [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U>, { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &[U; N]) -> bool { &&& (*self)@.len() == other@.len() &&& forall|i: int| #![auto] 0 <= i < (*self)@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec( &(*self)@[i], &other@[i], ) }}
// array == slice refpub assume_specification<'a, T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<&[U]>>::eq ]( left: &[T; N], right: &&[U],) -> bool;
impl<'a, T, U, const N: usize> super::cmp::PartialEqSpecImpl<&'a [U]> for [T; N] where T: PartialEq<U> + super::cmp::PartialEqSpec<U>, { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &&'a [U]) -> bool { &&& self@.len() == (*other)@.len() &&& forall|i: int| #![auto] 0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec( &self@[i], &(*other)@[i], ) }}
// slice == arraypub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T] as PartialEq<[U; N]>>::eq ]( left: &[T], right: &[U; N],) -> bool;
impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U>, { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &[U; N]) -> bool { &&& self@.len() == other@.len() &&& forall|i: int| #![auto] 0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec( &self@[i], &other@[i], ) }}
// array == slicepub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<[U]>>::eq ]( left: &[T; N], right: &[U],) -> bool;
impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U]> for [T; N] where T: PartialEq<U> + super::cmp::PartialEqSpec<U>, { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &[U]) -> bool { &&& self@.len() == other@.len() &&& forall|i: int| #![auto] 0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec( &self@[i], &other@[i], ) }}
} // verus!