Skip to content

add Countable instance for decidable Sigma types

Simon Gregersen requested to merge simongregersen/stdpp:countable_sig into master

This instance became useful when working with, e.g., a type for elements of a set { a : A | a ∈ X } and wanting to construct a gmap with this domain.

Merge request reports