src/Pure/General/rat.ML
changeset 19557 4866ebb16ba8
parent 17950 924d3e71cdc9
child 22189 10278e568741
equal deleted inserted replaced
19556:a3951e34269f 19557:4866ebb16ba8
     8 signature RAT =
     8 signature RAT =
     9 sig
     9 sig
    10   type rat
    10   type rat
    11   exception DIVZERO
    11   exception DIVZERO
    12   val zero: rat
    12   val zero: rat
       
    13   val one: rat
    13   val rat_of_int: int -> rat
    14   val rat_of_int: int -> rat
    14   val rat_of_intinf: IntInf.int -> rat
    15   val rat_of_intinf: IntInf.int -> rat
    15   val rat_of_quotient: IntInf.int * IntInf.int -> rat
    16   val rat_of_quotient: IntInf.int * IntInf.int -> rat
    16   val quotient_of_rat: rat -> IntInf.int * IntInf.int
    17   val quotient_of_rat: rat -> IntInf.int * IntInf.int
    17   val string_of_rat: rat -> string
    18   val string_of_rat: rat -> string
    37 datatype rat = Rat of bool * IntInf.int * IntInf.int;
    38 datatype rat = Rat of bool * IntInf.int * IntInf.int;
    38 
    39 
    39 exception DIVZERO;
    40 exception DIVZERO;
    40 
    41 
    41 val zero = Rat (true, 0, 1);
    42 val zero = Rat (true, 0, 1);
       
    43 
       
    44 val one = Rat (true, 1, 1);
    42 
    45 
    43 fun rat_of_intinf i =
    46 fun rat_of_intinf i =
    44   if i < 0
    47   if i < 0
    45   then Rat (false, ~i, 1)
    48   then Rat (false, ~i, 1)
    46   else Rat (true, i, 1);
    49   else Rat (true, i, 1);