ial/bool-kleene.agda at master · cedille/ial · GitHub

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
-- Kleene's three-valued logic

module bool-kleene where

open import bool
open import eq

data 𝔹ₖ : Set where
  tt : 𝔹ₖ
  ff : 𝔹ₖ
  uu : 𝔹ₖ

infix  7 ~ₖ_
infixr 6 _&&ₖ_
infixr 5 _||ₖ_
--infixr 4 _impₖ_

~ₖ_ : 𝔹ₖ → 𝔹ₖ
~ₖ tt = ff
~ₖ ff = tt
~ₖ uu = uu

-- and
_&&ₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
tt &&ₖ b = b
ff &&ₖ b = ff
uu &&ₖ ff = ff
uu &&ₖ b = uu

-- or
_||ₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
ff ||ₖ b = b
tt ||ₖ b = tt
uu ||ₖ tt = tt
uu ||ₖ b = uu

-- implication
_impₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
tt impₖ b2 = b2
ff impₖ b2 = tt
uu impₖ tt = tt
uu impₖ b = uu

knownₖ : 𝔹ₖ → 𝔹
knownₖ tt = tt
knownₖ ff = tt
knownₖ uu = ff

to-𝔹 : (b : 𝔹ₖ) → knownₖ b ≡ tt → 𝔹
to-𝔹 tt p = tt
to-𝔹 ff p = ff
to-𝔹 uu ()