vstd
Module seq_lib
Macros
Functions
In crate vstd
?
Settings
Module
vstd
::
seq_lib
Copy item path
source
·
[
−
]
Macros
§
assert_seqs_equal
Prove two sequences
s1
and
s2
are equal by proving that their elements are equal at each index.
Functions
§
commutative_foldr
group_seq_lib_default
lemma_append_last
lemma_concat_associative
lemma_flatten_alt_concat
lemma_flatten_concat
lemma_fold_right_permutation
lemma_max_of_concat
lemma_min_of_concat
lemma_multiset_commutative
lemma_no_dup_in_concat
lemma_seq_append_take_skip
lemma_seq_concat_contains_all_elements
lemma_seq_contains
lemma_seq_contains_after_push
lemma_seq_empty_contains_nothing
lemma_seq_empty_equality
lemma_seq_properties
lemma_seq_skip_build_commut
lemma_seq_skip_contains
lemma_seq_skip_index
lemma_seq_skip_index2
lemma_seq_skip_len
lemma_seq_skip_nothing
lemma_seq_skip_of_skip
lemma_seq_skip_update_commut1
lemma_seq_skip_update_commut2
lemma_seq_subrange_elements
lemma_seq_take_contains
lemma_seq_take_index
lemma_seq_take_len
lemma_seq_take_nothing
lemma_seq_take_update_commut1
lemma_seq_take_update_commut2
lemma_seq_union_to_multiset_commutative
lemma_sorted_unique
seq_to_set_is_finite
subrange_of_matching_take