Basic definition for decidable sets

A decidable set is one where one can decide member ship. I.E., there must be a function computing the member ship and decidable sets are formalized as _ bool.

Require Export misc.

Section Sets.

  Variable A : Type.

  Definition dset : Type := Abool.

  Definition dunion(P Q : dset) : dset := fun(a : A) ⇒ orb (P a) (Q a).

End Sets.

Implicit Arguments dunion [A].