vstd::raw_ptr

Function axiom_ptr_mut_from_data

Source
pub broadcast proof fn axiom_ptr_mut_from_data<T: ?Sized>(data: PtrData)
Expand description
ensures
(#[trigger] ptr_mut_from_data::<T>(data))@ == data,

The view of a pointer constructed from data: PtrData should be exactly that data.