# cogset

Add a type `cogset A`

of finite/cofinite sets of elements of countable type `A`

. When `A`

is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finite set.

The file includes efficient conversions to and from `gset A`

(for finite cogsets) and to `coPset`

(for arbitrary cogsets), as well as less efficient conversions to and from other finite sets and other sets with a top element.

Two things are marked TODO in the source, which really means "to discuss".