-
Notifications
You must be signed in to change notification settings - Fork 3
/
dk_char.dk
79 lines (73 loc) · 4.12 KB
/
dk_char.dk
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
76
77
78
79
#NAME dk_char.
(; 7bits (ascii) characters ;)
def char : cc.uT := dk_machine_int.Mint dk_nat.7.
def Char := cc.eT char.
def _O : dk_binary_nat.BNat := dk_binary_nat.O.
def S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0.
def S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1.
def cast : dk_binary_nat.BNat -> Char := dk_binary_nat.mnat_of_bnat dk_nat.7.
def 0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
def 9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
def A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
def B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
def a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
def b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
def __ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
def equal : Char -> Char -> cc.eT dk_bool.bool
:= dk_machine_int.equal dk_nat.7.