Function vstd::std_specs::vecdeque::axiom_spec_iter

source · 
pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>)
Expand description
ensures
(#[trigger] spec_iter(v))@ == (0int, v@),