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
:=
A
→
bool
.
Definition
dunion
(
P
Q
:
dset
) :
dset
:=
fun
(
a
:
A
) ⇒
orb
(
P
a
) (
Q
a
).
End
Sets
.
Implicit Arguments
dunion
[
A
].