Skip to main content

axiom_unpack_pack

vstd::mut_ref

Function axiom_unpack_pack 

Source 
pub broadcast proof fn axiom_unpack_pack<T: ?Sized>(data: MutRef<'_, T>)
Expand description
ensures
MutRef::unpack(#[trigger] data.pack()) == data,