Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Raphaël Cauderlier
dklib
Commits
4c4c64b3
Commit
4c4c64b3
authored
Nov 13, 2013
by
Raphaël Cauderlier
Browse files
[dk_char] Refactoring + underscore char
parent
80dac59f
Changes
1
Hide whitespace changes
Inline
Side-by-side
dk_char.dk
View file @
4c4c64b3
...
...
@@ -3,83 +3,82 @@
#IMPORT cc
#IMPORT dk_nat
UNat : Type := cc.eT dk_nat.Nat.
UO : UNat := dk_nat.O.
US : UNat -> UNat := dk_nat.S.
#IMPORT dk_binary_nat
#IMPORT dk_machine_int
char : cc.uT := dk_machine_int.Mint dk_nat.__7.
Char := cc.eT char.
_O : dk_binary_nat.N := dk_binary_nat.O.
S0 : dk_binary_nat.N -> dk_binary_nat.N := dk_binary_nat.S0.
S1 : dk_binary_nat.N -> dk_binary_nat.N := dk_binary_nat.S1.
cast : dk_binary_nat.N -> cc.eT char := dk_machine_int.cast_bnat dk_nat.__7.
cast : dk_binary_nat.N -> Char := dk_machine_int.cast_bnat dk_nat.__7.
_0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
_1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
_2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
_3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
_4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
_5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
_6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
_7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
_8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
_9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
_0 : cc.eT char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
_1 : cc.eT char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
_2 : cc.eT char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
_3 : cc.eT char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
_4 : cc.eT char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
_5 : cc.eT char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
_6 : cc.eT char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
_7 : cc.eT char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
_8 : cc.eT char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
_9 : cc.eT char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
A
:
cc.eT c
har := cast (S1 (S0 (S0 (S0 (S0 (S
0
(S1 _O))))))).
B
:
cc.eT c
har := cast (S0 (S1 (S0 (S0 (S0 (S
0
(S1 _O))))))).
C
:
cc.eT c
har := cast (S1 (S1 (S0 (S0 (S0 (S
0
(S1 _O))))))).
D
:
cc.eT c
har := cast (S0 (S0 (S1 (S0 (S0 (S
0
(S1 _O))))))).
E
:
cc.eT c
har := cast (S1 (S0 (S1 (S0 (S0 (S
0
(S1 _O))))))).
F
:
cc.eT c
har := cast (S0 (S1 (S1 (S0 (S0 (S
0
(S1 _O))))))).
G
:
cc.eT c
har := cast (S1 (S1 (S1 (S0 (S0 (S
0
(S1 _O))))))).
H
:
cc.eT c
har := cast (S0 (S0 (S0 (S1 (S0 (S
0
(S1 _O))))))).
I
:
cc.eT c
har := cast (S1 (S0 (S0 (S1 (S0 (S
0
(S1 _O))))))).
J
:
cc.eT c
har := cast (S0 (S1 (S0 (S1 (S0 (S
0
(S1 _O))))))).
K
:
cc.eT c
har := cast (S1 (S1 (S0 (S1 (S0 (S
0
(S1 _O))))))).
L
:
cc.eT c
har := cast (S0 (S0 (S1 (S1 (S0 (S
0
(S1 _O))))))).
M
:
cc.eT c
har := cast (S1 (S0 (S1 (S1 (S0 (S
0
(S1 _O))))))).
N
:
cc.eT c
har := cast (S0 (S1 (S1 (S1 (S0 (S
0
(S1 _O))))))).
O
:
cc.eT c
har := cast (S1 (S1 (S1 (S1 (S0 (S
0
(S1 _O))))))).
P
:
cc.eT c
har := cast (S0 (S0 (S0 (S0 (S1 (S
0
(S1 _O))))))).
Q
:
cc.eT c
har := cast (S1 (S0 (S0 (S0 (S1 (S
0
(S1 _O))))))).
R
:
cc.eT c
har := cast (S0 (S1 (S0 (S0 (S1 (S
0
(S1 _O))))))).
S
:
cc.eT c
har := cast (S1 (S1 (S0 (S0 (S1 (S
0
(S1 _O))))))).
T
:
cc.eT c
har := cast (S0 (S0 (S1 (S0 (S1 (S
0
(S1 _O))))))).
U
:
cc.eT c
har := cast (S1 (S0 (S1 (S0 (S1 (S
0
(S1 _O))))))).
V
:
cc.eT c
har := cast (S0 (S1 (S1 (S0 (S1 (S
0
(S1 _O))))))).
W
:
cc.eT c
har := cast (S1 (S1 (S1 (S0 (S1 (S
0
(S1 _O))))))).
X
:
cc.eT c
har := cast (S0 (S0 (S0 (S1 (S1 (S
0
(S1 _O))))))).
Y
:
cc.eT c
har := cast (S1 (S0 (S0 (S1 (S1 (S
0
(S1 _O))))))).
Z
:
cc.eT c
har := cast (S0 (S1 (S0 (S1 (S1 (S
0
(S1 _O))))))).
a
:
C
har := cast (S1 (S0 (S0 (S0 (S0 (S
1
(S1 _O))))))).
b
:
C
har := cast (S0 (S1 (S0 (S0 (S0 (S
1
(S1 _O))))))).
c
:
C
har := cast (S1 (S1 (S0 (S0 (S0 (S
1
(S1 _O))))))).
d
:
C
har := cast (S0 (S0 (S1 (S0 (S0 (S
1
(S1 _O))))))).
e
:
C
har := cast (S1 (S0 (S1 (S0 (S0 (S
1
(S1 _O))))))).
f
:
C
har := cast (S0 (S1 (S1 (S0 (S0 (S
1
(S1 _O))))))).
g
:
C
har := cast (S1 (S1 (S1 (S0 (S0 (S
1
(S1 _O))))))).
h
:
C
har := cast (S0 (S0 (S0 (S1 (S0 (S
1
(S1 _O))))))).
i
:
C
har := cast (S1 (S0 (S0 (S1 (S0 (S
1
(S1 _O))))))).
j
:
C
har := cast (S0 (S1 (S0 (S1 (S0 (S
1
(S1 _O))))))).
k
:
C
har := cast (S1 (S1 (S0 (S1 (S0 (S
1
(S1 _O))))))).
l
:
C
har := cast (S0 (S0 (S1 (S1 (S0 (S
1
(S1 _O))))))).
m
:
C
har := cast (S1 (S0 (S1 (S1 (S0 (S
1
(S1 _O))))))).
n
:
C
har := cast (S0 (S1 (S1 (S1 (S0 (S
1
(S1 _O))))))).
o
:
C
har := cast (S1 (S1 (S1 (S1 (S0 (S
1
(S1 _O))))))).
p
:
C
har := cast (S0 (S0 (S0 (S0 (S1 (S
1
(S1 _O))))))).
q
:
C
har := cast (S1 (S0 (S0 (S0 (S1 (S
1
(S1 _O))))))).
r
:
C
har := cast (S0 (S1 (S0 (S0 (S1 (S
1
(S1 _O))))))).
s
:
C
har := cast (S1 (S1 (S0 (S0 (S1 (S
1
(S1 _O))))))).
t
:
C
har := cast (S0 (S0 (S1 (S0 (S1 (S
1
(S1 _O))))))).
u
:
C
har := cast (S1 (S0 (S1 (S0 (S1 (S
1
(S1 _O))))))).
v
:
C
har := cast (S0 (S1 (S1 (S0 (S1 (S
1
(S1 _O))))))).
w
:
C
har := cast (S1 (S1 (S1 (S0 (S1 (S
1
(S1 _O))))))).
x
:
C
har := cast (S0 (S0 (S0 (S1 (S1 (S
1
(S1 _O))))))).
y
:
C
har := cast (S1 (S0 (S0 (S1 (S1 (S
1
(S1 _O))))))).
z
:
C
har := cast (S0 (S1 (S0 (S1 (S1 (S
1
(S1 _O))))))).
a : cc.eT char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
b : cc.eT char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
c : cc.eT char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
d : cc.eT char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
e : cc.eT char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
f : cc.eT char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
g : cc.eT char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
h : cc.eT char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
i : cc.eT char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
j : cc.eT char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
k : cc.eT char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
l : cc.eT char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
m : cc.eT char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
n : cc.eT char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
o : cc.eT char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
p : cc.eT char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
q : cc.eT char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
r : cc.eT char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
s : cc.eT char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
t : cc.eT char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
u : cc.eT char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
v : cc.eT char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
w : cc.eT char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
x : cc.eT char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
y : cc.eT char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
z : cc.eT char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
#IMPORT dk_bool
equal :
cc.eT char -> cc.eT c
har -> cc.eT dk_bool.bool := dk_machine_int.equal dk_nat.__7.
equal :
Char -> C
har -> cc.eT dk_bool.bool := dk_machine_int.equal dk_nat.__7.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
