Trait ObeysDeepEq 

pub trait ObeysDeepEq:
    Sized
    + PartialEq
    + DeepView {
    // Required method
    proof fn lemma_obeys_deep_eq();
}

Types whose Rust equality (==) decides deep-view equality.

Required Methods

proof fn lemma_obeys_deep_eq()

ensures

crate::laws_eq::obeys_deep_eq::<Self>(),

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl ObeysDeepEq for String

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for bool

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for char

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for i8

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for i16

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for i32

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for i64

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for i128

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for isize

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for u8

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for u16

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for u32

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for u64

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for u128

proof fn lemma_obeys_deep_eq()

impl ObeysDeepEq for usize

proof fn lemma_obeys_deep_eq()

impl<'a, T: ObeysDeepEq> ObeysDeepEq for &'a T

proof fn lemma_obeys_deep_eq()

impl<'a, T: ObeysDeepEq> ObeysDeepEq for &'a [T]

proof fn lemma_obeys_deep_eq()

impl<'a> ObeysDeepEq for &'a str

proof fn lemma_obeys_deep_eq()

impl<K: ObeysDeepEq + Hash + Eq, V: ObeysDeepEq> ObeysDeepEq for HashMap<K, V>

proof fn lemma_obeys_deep_eq()

impl<K: ObeysDeepEq + Hash + Eq> ObeysDeepEq for HashSet<K>

proof fn lemma_obeys_deep_eq()

impl<T0: ObeysDeepEq, T1: ObeysDeepEq, T2: ObeysDeepEq, T3: ObeysDeepEq> ObeysDeepEq for (T0, T1, T2, T3)

proof fn lemma_obeys_deep_eq()

impl<T0: ObeysDeepEq, T1: ObeysDeepEq, T2: ObeysDeepEq> ObeysDeepEq for (T0, T1, T2)

proof fn lemma_obeys_deep_eq()

impl<T0: ObeysDeepEq, T1: ObeysDeepEq> ObeysDeepEq for (T0, T1)

proof fn lemma_obeys_deep_eq()

impl<T0: ObeysDeepEq> ObeysDeepEq for (T0,)

proof fn lemma_obeys_deep_eq()

impl<T: ObeysDeepEq, E: ObeysDeepEq> ObeysDeepEq for Result<T, E>

proof fn lemma_obeys_deep_eq()

impl<T: ObeysDeepEq> ObeysDeepEq for Option<T>

proof fn lemma_obeys_deep_eq()

impl<T: ObeysDeepEq> ObeysDeepEq for Vec<T>

proof fn lemma_obeys_deep_eq()

Implementors

impl<T: ObeysDeepEq + Hash + Eq> ObeysDeepEq for ExecMultiset<T>

impl<T: ObeysDeepEq> ObeysDeepEq for ExecMemContents<T>