vstd::contrib::exec_spec

Trait ExecSpecEq

Source 
pub trait ExecSpecEq<'a>: DeepView + Sized {
    type Other: DeepView<V = Self::V>;

    // Required method
    exec fn exec_eq(this: Self, other: Self::Other) -> res : bool;
}
Expand description

Spec for the executable version of equality.

Required Associated Types§

Source

type Other: DeepView<V = Self::V>

Required Methods§

Source

exec fn exec_eq(this: Self, other: Self::Other) -> res : bool

ensures
res == (this.deep_view() =~~= other.deep_view()),

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<'a> ExecSpecEq<'a> for &'a bool

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a bool

Source§

impl<'a> ExecSpecEq<'a> for &'a char

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a char

Source§

impl<'a> ExecSpecEq<'a> for &'a i8

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a i8

Source§

impl<'a> ExecSpecEq<'a> for &'a i16

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a i16

Source§

impl<'a> ExecSpecEq<'a> for &'a i32

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a i32

Source§

impl<'a> ExecSpecEq<'a> for &'a i64

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a i64

Source§

impl<'a> ExecSpecEq<'a> for &'a i128

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a i128

Source§

impl<'a> ExecSpecEq<'a> for &'a isize

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a isize

Source§

impl<'a> ExecSpecEq<'a> for &'a str

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a str

Source§

impl<'a> ExecSpecEq<'a> for &'a u8

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a u8

Source§

impl<'a> ExecSpecEq<'a> for &'a u16

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a u16

Source§

impl<'a> ExecSpecEq<'a> for &'a u32

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a u32

Source§

impl<'a> ExecSpecEq<'a> for &'a u64

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a u64

Source§

impl<'a> ExecSpecEq<'a> for &'a u128

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a u128

Source§

impl<'a> ExecSpecEq<'a> for &'a usize

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a usize

Source§

impl<'a> ExecSpecEq<'a> for &'a String

Required for comparing, e.g., Vec<String>s.

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a String

Source§

impl<'a> ExecSpecEq<'a> for bool

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = bool

Source§

impl<'a> ExecSpecEq<'a> for char

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = char

Source§

impl<'a> ExecSpecEq<'a> for i8

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = i8

Source§

impl<'a> ExecSpecEq<'a> for i16

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = i16

Source§

impl<'a> ExecSpecEq<'a> for i32

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = i32

Source§

impl<'a> ExecSpecEq<'a> for i64

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = i64

Source§

impl<'a> ExecSpecEq<'a> for i128

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = i128

Source§

impl<'a> ExecSpecEq<'a> for isize

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = isize

Source§

impl<'a> ExecSpecEq<'a> for u8

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = u8

Source§

impl<'a> ExecSpecEq<'a> for u16

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = u16

Source§

impl<'a> ExecSpecEq<'a> for u32

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = u32

Source§

impl<'a> ExecSpecEq<'a> for u64

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = u64

Source§

impl<'a> ExecSpecEq<'a> for u128

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = u128

Source§

impl<'a> ExecSpecEq<'a> for usize

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = usize

Source§

impl<'a, T1: DeepView, T2: DeepView> ExecSpecEq<'a> for &'a (T1, T2)
where &'a T1: ExecSpecEq<'a, Other = &'a T1>, &'a T2: ExecSpecEq<'a, Other = &'a T2>,

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a (T1, T2)

Source§

impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Option<T>
where &'a T: ExecSpecEq<'a, Other = &'a T>,

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a Option<T>

Source§

impl<'a, T: DeepView> ExecSpecEq<'a> for &'a [T]
where &'a T: ExecSpecEq<'a, Other = &'a T>,

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a [T]

Source§

impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Vec<T>
where &'a T: ExecSpecEq<'a, Other = &'a T>,

Source§

exec fn exec_eq(this: Self, other: Self::Other) -> bool

Source§

type Other = &'a Vec<T>

Implementors§