Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 21 Sep 1993 10:54:59 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA17752; Tue, 21 Sep 93 02:47:36 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA17748; Tue, 21 Sep 93 02:47:29 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Tue, 21 Sep 93 10:19:11 BST From: David Shepherd Message-Id: <14980.9309210947@frogland.inmos.co.uk> Subject: integer division (pref in hol90) To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Tue, 21 Sep 1993 10:46:59 +0100 (BST) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 920 hol90's integer library contains a definition of (one of the several possible) integer division operators, but there are no further theorems developed from it, whereas DIV and MOD have several uniqueness theorems etc. 1) has anyone proved the equivalent uniqueness theorems etc for integer div and mod. 2) also, has anyone already developed a "2 complement"/"round zero" style division - i.e. where the remainder lies in the interval [-D/2,D/2) (well at least for a positive divisor D). this is needed to associate a (truncated) word with an arbitary integer value. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "They didn't like the rates, they don't like the poll tax, and they won't like the council tax." - Nicholas Ridley