Function spec_slice_is_empty Copy item path

pub open spec fn spec_slice_is_empty<T>(slice: &[T]) -> bool

{ slice@.len() == 0 }