Skip to main content

mut_ref_slice_len_eq

vstd::slice

Function mut_ref_slice_len_eq 

Source 
pub proof fn mut_ref_slice_len_eq<T>(tracked slice: &&mut [T])
Expand description
ensures
old(*slice).len() == final(*slice).len(),