{-# OPTIONS --cubical-compatible #-}

module Terra.Data.Bool where
open import Agda.Builtin.Bool public
open import Terra.Data.Level.Variables


-- data Bool : Set where
--   true : Bool
--   false : Bool

-- {-# BUILTIN BOOL  Bool  #-}
-- {-# BUILTIN TRUE  true  #-}
-- {-# BUILTIN FALSE false #-}

if_then_else_ : {A : Set ℓ} -> Bool -> A -> A -> A
if true then y else n = y
if false then y else n = n

not : Bool -> Bool
not true = false
not false = true

_xor_ : Bool -> Bool -> Bool
false xor b = b
true xor b = not b