{-# 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
open import Agda.Builtin.Bool public
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
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
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
T : Bool → Set
T true = ⊤
T false = ⊥