Module seq

Source

Macros§

seq
Creates a Seq containing the given elements.

Structs§

Seq
Seq<A> is a sequence type for specifications. To use a “sequence” in compiled code, use an exec type like vec::Vec that has Seq<A> as its specification type.

Functions§

axiom_seq_add_index1
axiom_seq_add_index2
axiom_seq_add_len
axiom_seq_empty
axiom_seq_ext_equal
axiom_seq_ext_equal_deep
axiom_seq_index_decreases
axiom_seq_len_decreases
axiom_seq_new_index
axiom_seq_new_len
axiom_seq_push_index_different
axiom_seq_push_index_same
axiom_seq_push_len
axiom_seq_subrange_decreases
axiom_seq_subrange_index
axiom_seq_subrange_len
axiom_seq_update_different
axiom_seq_update_len
axiom_seq_update_same
group_seq_axioms