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