Skip to main content

axiom_view_ptr_mut_eq

vstd_extra::external::nonnull

Function axiom_view_ptr_mut_eq 

Source 
pub broadcast proof fn axiom_view_ptr_mut_eq<T: PointeeSized>(a: NonNull<T>)
Expand description
ensures
nonnull_from_ptr_mut_spec(#[trigger] a.view_ptr_mut()) == a,

The NonNull constructed from the view of a NonNull<T> should be exactly that NonNull<T>. Implies that a.view_ptr_mut() == b.view_ptr_mut() ==> a == b.