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