Module vstd::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