{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude

module Bool where

infix    if_then_else_

infixr   _∨_ _xor_
infixr   _∧_

----------------------------------------

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

----------------------------------------