axiom_ptr_mut_from_nonnull_eq

Function axiom_ptr_mut_from_nonnull_eq 

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