module Decide where

open import Logic

data Dec P : Set where
  no  : (np : ¬ P)  Dec P
  yes : (p  :   P)  Dec P

open import Bool

unbool : (x : Bool)  Dec (IsTrue x)
unbool true = yes tt
unbool false = no  x  x)