Module set_lib
vstd
Module set_lib
Re-exports
Macros
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
::
set_lib
Copy item path
source
·
[
−
]
Re-exports
§
pub use assert_sets_equal_internal;
Macros
§
assert_
sets_
equal
Prove two sets equal by extensionality. Usage is:
Functions
§
axiom_
is_
empty
axiom_
is_
empty_
len0
group_
set_
lib_
default
group_
set_
properties
lemma_
int_
range
lemma_
len_
difference
lemma_
len_
intersect
lemma_
len_
subset
lemma_
len_
union
lemma_
len_
union_
ind
lemma_
map_
size
lemma_
set_
difference2
lemma_
set_
difference_
len
lemma_
set_
disjoint
lemma_
set_
disjoint_
lens
lemma_
set_
empty_
equivalency_
len
lemma_
set_
insert_
finite_
iff
lemma_
set_
intersect_
again1
lemma_
set_
intersect_
again2
lemma_
set_
intersect_
union_
lens
lemma_
set_
properties
Deprecated
lemma_
set_
remove_
finite_
iff
lemma_
set_
subset_
finite
lemma_
set_
union_
again1
lemma_
set_
union_
again2
lemma_
set_
union_
finite_
iff
lemma_
set_
union_
finite_
implies_
sets_
finite
lemma_
subset_
equality
set_
int_
range