☰
vstd
Module seq
Macros
Structs
Functions
In crate vstd
?
Module
vstd
::
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