pub broadcast proof fn axiom_nonnull_is_nonnull<T: PointeeSized>(ptr: NonNull<T>)Expand description
ensures
(#[trigger] ptr_mut_from_nonnull(ptr))@.addr != 0,pub broadcast proof fn axiom_nonnull_is_nonnull<T: PointeeSized>(ptr: NonNull<T>)(#[trigger] ptr_mut_from_nonnull(ptr))@.addr != 0,