------------------------------------------------------------------------
-- The Agda standard library
--
-- The type for booleans and some operations
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --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  _≤_ _<_
 
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  _∧_
infixr  _∨_ _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
 
------------------------------------------------------------------------
-- Conversion to Set
 
-- A function mapping true to an inhabited type and false to an empty
-- type.
T : Bool → Set
T true  = ⊤
T false = ⊥
 
------------------------------------------------------------------------
-- Other operations
 
infix  if_then_else_
 
if_then_else_ : Bool → A → A → A
if true  then t else f = t
if false then t else f = f