Re: Is this OK?

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>]

> (* 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