module Data.Bool where
open import Data.Function
open import Data.Unit
open import Data.Empty
open import Relation.Nullary.Core
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
infixr 6 _∧_
infixr 5 _∨_ _xor_
infix 0 if_then_else_
data Bool : Set where
true : Bool
false : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}
not : Bool → Bool
not true = false
not false = true
T : Bool → Set
T true = ⊤
T false = ⊥
if_then_else_ : {a : Set} → Bool → a → a → a
if true then t else f = t
if false then t else f = f
_∧_ : 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
_Bool-≟_ : Decidable {Bool} _≡_
true Bool-≟ true = yes ≡-refl
false Bool-≟ false = yes ≡-refl
true Bool-≟ false = no λ()
false Bool-≟ true = no λ()
Bool-preorder : Preorder
Bool-preorder = ≡-preorder Bool
Bool-setoid : Setoid
Bool-setoid = ≡-setoid Bool
Bool-decSetoid : DecSetoid
Bool-decSetoid = ≡-decSetoid _Bool-≟_