Macros§
- assert_
sets_ equal - Prove two sets equal by extensionality. Usage is:
Traits§
Functions§
- full_
set_ properties - 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_
map_ size_ bound - lemma_
set_ difference2 - lemma_
set_ difference_ len - lemma_
set_ disjoint - lemma_
set_ disjoint_ iff_ empty_ intersection - lemma_
set_ disjoint_ lens - lemma_
set_ empty_ equivalency_ len - lemma_
set_ intersect_ again1 - lemma_
set_ intersect_ again2 - lemma_
set_ intersect_ union_ lens - lemma_
set_ is_ empty - lemma_
set_ is_ empty_ len0 - lemma_
set_ union_ again1 - lemma_
set_ union_ again2 - lemma_
sets_ eq_ iff_ injective_ map_ eq - lemma_
sets_ eq_ iff_ injective_ map_ on_ eq - lemma_
subset_ equality - range_
set_ properties - set_
int_ range