diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
| commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
| tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/extraction/test/addReals | |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/extraction/test/addReals')
| -rw-r--r-- | contrib/extraction/test/addReals | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals new file mode 100644 index 00000000..fb73d47b --- /dev/null +++ b/contrib/extraction/test/addReals @@ -0,0 +1,21 @@ +open TypeSyntax +open Fast_integer + + +let total_order_T x y = +if x = y then InleftT RightT +else if x < y then InleftT LeftT +else InrightT + +let rec int_to_positive i = + if i = 1 then XH + else + if (i mod 2) = 0 then XO (int_to_positive (i/2)) + else XI (int_to_positive (i/2)) + +let rec int_to_Z i = + if i = 0 then ZERO + else if i > 0 then POS (int_to_positive i) + else NEG (int_to_positive (-i)) + +let my_ceil x = int_to_Z (succ (int_of_float (floor x))) |