module Prelude.Decidable where

open import Prelude.Empty

data Dec {a} (P : Set a) : Set a where
  yes : P → Dec P
  no  : ¬ P → Dec P

infix  ifYes_then_else_ ifNo_then_else_
ifYes_then_else_ : ∀ {a b} {A : Set a} {B : Set b} → Dec A → B → B → B
ifYes yes _ then x else _ = x
ifYes no  _ then _ else y = y

ifNo_then_else_ : ∀ {a b} {A : Set a} {B : Set b} → Dec A → B → B → B
ifNo d then x else y = ifYes d then y else x