diff options
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))) |