Function vstd::raw_ptr::ptrs_mut_eq

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

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