Skip to main content

axiom_seq_index_decreases

Function axiom_seq_index_decreases 

Source
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])),