/
Base.agda
75 lines (54 loc) · 1.62 KB
/
Base.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
------------------------------------------------------------------------
-- 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 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
------------------------------------------------------------------------
-- 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 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