Settings
Help
group_multiset_properties
vstd
In vstd::
multiset
Macros
assert_multisets_equal
Structs
Multiset
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_properties
lemma_right_pseudo_idempotence
lemma_update_different
lemma_update_same
vstd
::
multiset
Function
group_
multiset_
properties
Copy item path
Source
Search
Settings
Help
Summary
pub
broadcast group
fn group_multiset_properties()
Expand description
broadcast group