vstd::raw_ptr

Function ptrs_mut_eq

Source 
pub broadcast proof fn ptrs_mut_eq<T: ?Sized>(a: *mut T)
Expand description
ensures
view_reverse_for_eq::<T>(#[trigger] a@) == a,

Implies that a@ == b@ ==> a == b.