[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...> |
| Subject: | Re: Is this OK? |
> (* a camllight session *) > > #(-234)/4 > ;; > - : int = -58 > > > #div_big_int (big_int_of_string "-234") (big_int_of_string "4");; > - : big_int = -59 There is OK. Indeed, when defining the quotient and the remainder you must specify the range of the remainder. Usually, you specify that the remainder of the division of a by b is between 0 and b-1, whatever is the sign of a. That is the case in the big_in library. But in the case of Caml division, the specification is different: the remainder has the same sign that a, which is negative in your example. But in both cases you always have a = b * (a/b) + (a mod b) which is the expected invariant. -- Jean-Christophe FILLIATRE mailto:Jean-Christophe.Filliatre@lri.fr http://www.lri.fr/~filliatr