1signature Arbrat =
2sig
3
4  eqtype rat
5
6  type num = Arbnum.num
7  type aint = Arbint.int
8
9  val zero       : rat
10  val one        : rat
11  val two        : rat
12  val numerator  : rat -> aint
13  val denominator: rat -> num
14
15  val toString   : rat -> string
16  val fromString : string -> rat  (* only integral forms *)
17
18  val fromInt    : Int.int -> rat
19  val fromAInt   : aint -> rat
20  val fromNat    : num -> rat
21
22  val toAInt     : rat -> aint
23  val toInt      : rat -> Int.int
24  val toNat      : rat -> num
25
26  val +          : (rat * rat) -> rat
27  val -          : (rat * rat) -> rat
28  val *          : (rat * rat) -> rat
29  val /          : (rat * rat) -> rat
30  val inv        : rat -> rat
31  val negate     : rat -> rat
32  val ~          : rat -> rat
33  val abs        : rat -> rat
34
35  val <          : rat * rat -> bool
36  val <=         : rat * rat -> bool
37  val >          : rat * rat -> bool
38  val >=         : rat * rat -> bool
39
40  val compare    : rat * rat -> order
41  val min        : rat * rat -> rat
42  val max        : rat * rat -> rat
43
44  val floor      : rat -> aint
45  val ceil       : rat -> aint
46
47  val pp_rat     : rat -> HOLPP.pretty
48
49end
50