Module vstd::set_lib

Re-exports

• pub use assert_sets_equal_internal;

Macros

• assert_sets_equal
  Prove two sets equal by extensionality. Usage is:

Functions

• axiom_is_empty
• group_set_lib_axioms
• 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_propertiesDeprecated
• lemma_set_remove_finite_iff
• 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