Function axiom_vec_dequeue_index_decreases

Help

pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)

Expand description

requires

0 <= i < v.len(),

ensures

#[trigger] (decreases_to!(v => v[i])),

Function axiom_vec_dequeue_index_decreasesCopy item path