open import NeilPrelude
module Data.Bool where
infix 0 if_then_else_
infixr 5 _∨_ _xor_
infixr 6 _∧_
----------------------------------------
not : Bool → Bool
not false = true
not true = false
if_then_else_ : {A : Set} → Bool → A → A → A
if_then_else_ false t e = e
if_then_else_ true t e = t
ifte : {A : Set} → A → A → Bool → A
ifte t e false = e
ifte t e true = t
_∧_ : Bool → Bool → Bool
true ∧ b = b
false ∧ b = false
_∨_ : Bool → Bool → Bool
true ∨ b = true
false ∨ b = b
_xor_ : Bool → Bool → Bool
true xor b = not b
false xor b = b
----------------------------------------