axiom_ptr_mut_from_nonull_eq

vstd_extra::external::nonnull

Function axiom_ptr_mut_from_nonull_eq 

Source 
pub broadcast proof fn axiom_ptr_mut_from_nonull_eq<T: PointeeSized>(ptr: NonNull<T>)
Expand description
ensures
nonnull_from_ptr_mut(#[trigger] ptr_mut_from_nonull(ptr)) == ptr,