File: addReals

package info (click to toggle)
coq 8.0pl2-2
  • links: PTS
  • area: main
  • in suites: sarge
  • size: 14,228 kB
  • ctags: 17,685
  • sloc: ml: 97,070; makefile: 1,255; sh: 738; lisp: 456; awk: 15
file content (21 lines) | stat: -rw-r--r-- 457 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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)))