layout_of_slices

Function layout_of_slices 

Source
pub broadcast proof fn layout_of_slices<T>(x: &[T])
Expand description
ensures
spec_align_of_val::<[T]>(x) == align_of::<T>(),
spec_size_of_val::<[T]>(x) == x@.len() * size_of::<T>(),

Slices have the same layout as the underlying type. (Reference).