Module set 

Modules

fold

Macros

set

Structs

Set

Set<A> is a finite set type for specifications.

Functions

axiom_set_ext_equal

axiom_set_ext_equal_deep

group_set_lemmas

lemma_set_choose_len

lemma_set_complement

lemma_set_contains_len

lemma_set_difference

lemma_set_empty

lemma_set_empty_len

lemma_set_filter

lemma_set_insert_different

lemma_set_insert_len

lemma_set_insert_same

lemma_set_intersect

lemma_set_new

lemma_set_new_assuming_finite

lemma_set_new_from_iset

lemma_set_new_some

lemma_set_remove_different

lemma_set_remove_insert

lemma_set_remove_len

lemma_set_remove_same

lemma_set_union

lemma_to_iset_finite

lemma_to_iset_len