------------------------------------------------------------------------
-- The Agda standard library
--
-- The type for booleans and some operations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Bool.Base where

open import Data.Unit.Base using ()
open import Data.Empty
open import Level using (Level)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- The boolean type

open import Agda.Builtin.Bool public

------------------------------------------------------------------------
-- Relations

infix 4 _≤_ _<_

data _≤_ : Bool  Bool  Set where
  f≤t : false  true
  b≤b :  {b}  b  b

data _<_ : Bool  Bool  Set where
  f<t : false < true

------------------------------------------------------------------------
-- Boolean operations

infixr 6 _∧_
infixr 5 _∨_ _xor_

not : Bool  Bool
not true  = false
not false = true

_∧_ : 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

------------------------------------------------------------------------
-- Other operations

infix  0 if_then_else_

if_then_else_ : Bool  A  A  A
if true  then t else f = t
if false then t else f = f

-- A function mapping true to an inhabited type and false to an empty
-- type.

T : Bool  Set
T true  = 
T false =