Module seq_lib

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_foldl
commutative_foldr
group_filter_ensures
group_seq_lib_default
group_seq_properties
group_to_multiset_ensures
lemma_append_last
lemma_concat_associative
lemma_exactly_one_view
lemma_filter_view_commute
lemma_flatten_alt_concat
lemma_flatten_concat
lemma_fold_left_permutation
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_propertiesDeprecated
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
lemma_update_is_remove_insert
seq_to_set_distributes_over_add
seq_to_set_is_finite
subrange_of_matching_take
to_multiset_build
to_multiset_contains
to_multiset_insert
to_multiset_len
to_multiset_remove
to_multiset_update