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