Module multiset
vstd
Module multiset
Macros
Structs
Functions
In crate vstd
Modules
arithmetic
array
atomic
atomic_ghost
bits
bytes
calc_macro
cell
compute
hash_map
hash_set
invariant
layout
map
map_lib
math
modes
multiset
multiset_lib
pcm
pcm_lib
pervasive
prelude
proph
raw_ptr
relations
rwlock
seq
seq_lib
set
set_lib
shared
simple_pptr
slice
std_specs
storage_protocol
string
thread
tokens
view
Macros
assert_by_contradiction
assert_maps_equal
assert_multisets_equal
assert_multisets_equal_internal
assert_seqs_equal
assert_sets_equal
atomic_with_ghost
calc
map
open_atomic_invariant
open_atomic_invariant_in_proof
open_atomic_invariant_in_proof_internal
open_atomic_invariant_internal
open_local_invariant
open_local_invariant_in_proof
open_local_invariant_in_proof_internal
open_local_invariant_internal
pcell_opt
pcell_points
seq
set
vpanic
Functions
group_vstd_default
?
Settings
Module
vstd
::
multiset
Copy item path
source
·
[
−
]
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_
properties
Deprecated
lemma_
right_
pseudo_
idempotence
lemma_
update_
different
lemma_
update_
same