Function vstd::std_specs::vecdeque::axiom_spec_len

source · 
pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &VecDeque<T, A>)
Expand description
ensures
#[trigger] spec_vec_dequeue_len(v) == v@.len(),