pub broadcast proof fn axiom_nonnull_from_ptr_mut_spec_eq<T: PointeeSized>(ptr: *mut T)Expand description
requires
ptr@.addr != 0,(#[trigger] nonnull_from_ptr_mut_spec(ptr)).view_ptr_mut() == ptr,The view of a NonNull<T> constructed from *mut T should be exactly that *mut T.