{-# OPTIONS --universe-polymorphism #-}
module Data.Bool where
open import Function
open import Data.Unit using (⊤)
open import Data.Empty
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl)
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 #-}
{-# COMPILED_DATA Bool Bool True False #-}
not : Bool → Bool
not true = false
not false = true
T : Bool → Set
T true = ⊤
T false = ⊥
if_then_else_ : ∀ {a} {A : Set a} → 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
_≟_ : Decidable {A = Bool} _≡_
true ≟ true = yes refl
false ≟ false = yes refl
true ≟ false = no λ()
false ≟ true = no λ()
decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_