Skip to main content

axiom_seq_new_index

Function axiom_seq_new_index 

Source
pub fn axiom_seq_new_index<A>(len: nat, f: FnSpec<(int,), A>, i: int)
👎Deprecated:

Seq axioms have been verified, and are now lemmas

Expand description
requires
0 <= i < len,
ensures
#[trigger] Seq::new(len, f)[i] == f(i),