------------------------------------------------------------------------ -- 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 =