Function vstd::std_specs::vec::axiom_vec_index_decreases

source · 
pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int)
Expand description
requires
0 <= i < v.len(),
ensures
#[trigger] (decreases_to!(v => v[i])),