Modules§
- fold
- This module defines a fold function for finite sets and proves a number of associated lemmas.
Macros§
Structs§
- ISet
ISet<A>is a set type for specifications.
Functions§
- group_
iset_ lemmas - lemma_
iset_ choose_ infinite - lemma_
iset_ choose_ len - lemma_
iset_ complement - lemma_
iset_ contains_ len - lemma_
iset_ difference - lemma_
iset_ difference_ finite - lemma_
iset_ empty - lemma_
iset_ empty_ finite - lemma_
iset_ empty_ len - lemma_
iset_ ext_ equal - lemma_
iset_ ext_ equal_ deep - lemma_
iset_ finite_ if_ subset_ of_ seq - lemma_
iset_ insert_ different - lemma_
iset_ insert_ finite - lemma_
iset_ insert_ len - lemma_
iset_ insert_ same - lemma_
iset_ intersect - lemma_
iset_ intersect_ finite - lemma_
iset_ mk_ map_ domain - lemma_
iset_ mk_ map_ index - lemma_
iset_ new - lemma_
iset_ remove_ different - lemma_
iset_ remove_ finite - lemma_
iset_ remove_ insert - lemma_
iset_ remove_ len - lemma_
iset_ remove_ same - lemma_
iset_ union - lemma_
iset_ union_ finite