blob: c181656f8734f257b4aa2eabdcfbbb05053db65b (
plain)
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
|
abstract Bin = {
cat Nat ; Bin ; Pos ;
data
Zero : Nat ;
Succ : Nat -> Nat ;
BZero : Bin ; -- 0
BPos : Pos -> Bin ; -- p
BOne : Pos ; -- 1
AZero : Pos -> Pos ; -- p0
AOne : Pos -> Pos ; -- p1
fun
bin2nat : Bin -> Nat ;
def
bin2nat BZero = Zero ;
bin2nat (BPos p) = pos2nat p ;
fun
pos2nat : Pos -> Nat ;
def
pos2nat BOne = one ;
pos2nat (AZero p) = twice (pos2nat p) ;
pos2nat (AOne p) = Succ (twice (pos2nat p)) ;
fun one : Nat ;
def one = Succ Zero ;
fun twice : Nat -> Nat ;
def
twice Zero = Zero ;
twice (Succ n) = Succ (Succ (twice n)) ;
fun
nat2bin : Nat -> Bin ;
def
nat2bin Zero = BZero ;
nat2bin (Succ n) = bSucc (nat2bin n) ;
fun
bSucc : Bin -> Bin ;
def
bSucc BZero = BPos BOne ;
bSucc (BPos p) = BPos (pSucc p) ;
fun
pSucc : Pos -> Pos ;
def
pSucc BOne = AZero BOne ;
pSucc (AZero p) = AOne p ;
pSucc (AOne p) = AZero (pSucc p) ;
}
|
