diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-23 15:00:02 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-23 15:00:02 +0000 |
| commit | 4135940aa7959b459735d2b4004dc77309fef2d7 (patch) | |
| tree | 943b52da07a1ca4ebc9eca191343f665489150c6 /contrib/extraction/test | |
| parent | bdbe617da66a314ab88eddfc796de1549359779e (diff) | |
realisation des reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test')
| -rw-r--r-- | contrib/extraction/test/addReals.ml | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/contrib/extraction/test/addReals.ml b/contrib/extraction/test/addReals.ml new file mode 100644 index 000000000..86e9a7994 --- /dev/null +++ b/contrib/extraction/test/addReals.ml @@ -0,0 +1,25 @@ +let total_order_T x y = +if x = y then + TypeSyntax.Coq_inleftT TypeSyntax.Coq_rightT +else if x < y then + TypeSyntax.Coq_inleftT TypeSyntax.Coq_leftT +else TypeSyntax.Coq_inrightT + +let rec int_to_positive i = + if i = 1 then + Fast_integer.Coq_xH + else + if (i mod 2) = 0 then + Fast_integer.Coq_xO (int_to_positive (i/2)) + else + Fast_integer.Coq_xI (int_to_positive (i/2)) + +let rec int_to_Z i = + if i = 0 then + Fast_integer.ZERO + else if i > 0 then + Fast_integer.POS (int_to_positive i) + else + Fast_integer.NEG (int_to_positive (-i)) + +let my_ceil x = int_to_Z (int_of_float (ceil x)) |