Skip to content

cogset

David Swasey requested to merge swasey/coq-stdpp:cogset into master

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".

Edited by David Swasey

Merge request reports