pub fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int)👎Deprecated:
Seq axioms have been verified, and are now lemmas
Expand description
requires
0 <= i < s.len(),ensures#[trigger] (decreases_to!(s => s[i])),