Module seq

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