numberBases.dk 3.13 KB
Newer Older
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
Figure : Type.
0 : Figure.
1 : Figure.
2 : Figure.
3 : Figure.
4 : Figure.
5 : Figure.
6 : Figure.
7 : Figure.
8 : Figure.
9 : Figure.
A : Figure.
B : Figure.
C : Figure.
D : Figure.
E : Figure.
F : Figure.

Number : Type.
Zero : Number.
Cons : Number -> Figure -> Number.

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
23 24
def decimal : tuto.Nat -> Number.
def decimal_aux : tuto.Nat -> Number -> Number.
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
25 26 27

[n] decimal n --> decimal_aux n Zero.

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
28 29 30 31 32 33 34 35 36 37 38 39
[N]   decimal_aux tuto.0     N          --> N.
[n]   decimal_aux (tuto.S n) Zero       --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (tuto.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (tuto.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (tuto.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (tuto.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (tuto.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (tuto.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (tuto.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (tuto.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (tuto.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (tuto.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
40

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
41 42
def binary : tuto.Nat -> Number.
def binary_aux : tuto.Nat -> Number -> Number.
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
43 44 45

[n] binary n --> binary_aux n Zero.

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
46 47 48 49
[N]   binary_aux tuto.0     N          --> N.
[n]   binary_aux (tuto.S n) Zero       --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (tuto.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (tuto.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
50

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
51 52
def hexadecimal : tuto.Nat -> Number.
def hexadecimal_aux : tuto.Nat -> Number -> Number.
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
53 54 55

[n] hexadecimal n --> hexadecimal_aux n Zero.

Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
[N]   hexadecimal_aux tuto.0     N          --> N.
[n]   hexadecimal_aux (tuto.S n) Zero       --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (tuto.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (tuto.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (tuto.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (tuto.S tuto.0) N) 0).
Guillaume GENESTIER's avatar
Forme  
Guillaume GENESTIER committed
74