From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA22148 for caml-redistribution; Mon, 18 May 1998 15:36:46 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA12785 for ; Mon, 18 May 1998 10:03:45 +0200 (MET DST) Received: from lri.lri.fr (root@lri.lri.fr [129.175.15.1]) by nez-perce.inria.fr (8.8.7/8.8.5) with ESMTP id KAA25110 for ; Mon, 18 May 1998 10:03:43 +0200 (MET DST) Received: from pc85.lri.fr (filliatr@pc85.lri.fr [129.175.8.105]) by lri.lri.fr (8.8.5/jtpda-5.2) with ESMTP id KAA09878 ; Mon, 18 May 1998 10:03:39 +0200 (MET DST) Received: by pc85.lri.fr (8.8.5/feuille) id KAA00738 ; Mon, 18 May 1998 10:03:53 +0200 Date: Mon, 18 May 1998 10:03:53 +0200 Message-Id: <199805180803.KAA00738@pc85.lri.fr> From: Jean-Christophe Filliatre MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: N Hur Cc: caml-list@inria.fr Subject: Re: Is this OK? In-Reply-To: References: X-Mailer: VM 6.34 under Emacs 19.34.1 Reply-To: Jean-Christophe.Filliatre@lri.fr (Jean-Christophe Filliatre) Sender: weis > (* 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