Module 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

group_multiset_properties

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_propertiesDeprecated

lemma_right_pseudo_idempotence

lemma_update_different

lemma_update_same