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_index1Deprecated

axiom_seq_add_index2Deprecated

axiom_seq_add_lenDeprecated

axiom_seq_emptyDeprecated

axiom_seq_ext_equalDeprecated

axiom_seq_ext_equal_deepDeprecated

axiom_seq_index_decreasesDeprecated

axiom_seq_len_decreases

axiom_seq_new_indexDeprecated

axiom_seq_new_lenDeprecated

axiom_seq_push_index_differentDeprecated

axiom_seq_push_index_sameDeprecated

axiom_seq_push_lenDeprecated

axiom_seq_subrange_decreasesDeprecated

axiom_seq_subrange_indexDeprecated

axiom_seq_subrange_lenDeprecated

axiom_seq_update_differentDeprecated

axiom_seq_update_lenDeprecated

axiom_seq_update_sameDeprecated

group_seq_axiomsDeprecated

group_seq_lemmas

group_seq_lemmas_expensive

lemma_seq_add_index1

lemma_seq_add_index2

lemma_seq_add_index1_alt

lemma_seq_add_index2_alt

lemma_seq_add_len

lemma_seq_empty

lemma_seq_ext_equal

lemma_seq_ext_equal_deep

lemma_seq_index_decreases

lemma_seq_new_index

lemma_seq_new_len

lemma_seq_push_index_different

lemma_seq_push_index_different_alt

lemma_seq_push_index_same

lemma_seq_push_len

lemma_seq_subrange_composition

lemma_seq_subrange_decreases

lemma_seq_subrange_index

lemma_seq_subrange_index_alt

lemma_seq_subrange_len

lemma_seq_two_subranges_index

lemma_seq_update_different

lemma_seq_update_different_alt

lemma_seq_update_len

lemma_seq_update_same

lemma_seq_update_same_alt