equal
deleted
inserted
replaced
23 |
23 |
24 The representation expects that @{text "(m mod 2)"} is 0 or 1, |
24 The representation expects that @{text "(m mod 2)"} is 0 or 1, |
25 even if m is negative; |
25 even if m is negative; |
26 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus |
26 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus |
27 @{text "-5 = (-3)*2 + 1"}. |
27 @{text "-5 = (-3)*2 + 1"}. |
|
28 |
|
29 This two's complement binary representation derives from the paper |
|
30 "An Efficient Representation of Arithmetic for Term Rewriting" by |
|
31 Dave Cohen and Phil Watson, Rewriting Techniques and Applications, |
|
32 Springer LNCS 488 (240-251), 1991. |
28 *} |
33 *} |
29 |
34 |
30 datatype bit = B0 | B1 |
35 datatype bit = B0 | B1 |
31 |
36 |
32 text{* |
37 text{* |