Skip to main content

length_slice

vest_lib::combinators::star::exec

Function length_slice 

Source 
pub exec fn length_slice<Inner, T>(fmt: &Inner, values: &[T]) -> len : usize
where
    Inner: ByteLen<T>,
    T: DeepView,
Expand description
requires
fmt.exec_inv(),
(super::Star(*fmt)).byte_len(values.deep_view()) <= usize::MAX,
ensures
len == (super::Star(*fmt)).byte_len(values.deep_view()),