Module vstd::multiset

Macros

• assert_multisets_equal

Structs

• Multiset
  Multiset<V> is an abstract multiset type for specifications.

Functions

• axiom_choose_count
• axiom_count_le_len
• axiom_filter_count
• axiom_len_add
• axiom_len_empty
• axiom_len_singleton
• axiom_len_sub
• axiom_multiset_add
• axiom_multiset_always_finite
• axiom_multiset_contained
• axiom_multiset_empty
• axiom_multiset_ext_equal
• axiom_multiset_ext_equal_deep
• axiom_multiset_new_not_contained
• axiom_multiset_singleton
• axiom_multiset_singleton_different
• axiom_multiset_sub
• group_multiset_axioms
• lemma_difference_bottoms_out
• lemma_difference_count
• lemma_insert_containment
• lemma_insert_increases_count_by_1
• lemma_insert_len
• lemma_insert_non_decreasing
• lemma_insert_other_elements_unchanged
• lemma_intersection_count
• lemma_left_pseudo_idempotence
• lemma_multiset_empty_len
• lemma_multiset_properties
• lemma_right_pseudo_idempotence
• lemma_update_different
• lemma_update_same