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; Thu, 26 Aug 1993 09:33:51 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03456; Thu, 26 Aug 93 01:22:55 -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 AA03452; Thu, 26 Aug 93 01:22:50 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 26 Aug 93 09:22:44 BST From: David Shepherd Message-Id: <18817.9308260822@frogland.inmos.co.uk> Subject: Re: numerals by pretty printer instead by num_CONV? To: info-hol@dworshak.cs.uidaho.edu (info-hol mailing list) Date: Thu, 26 Aug 1993 09:22:24 +0100 (BST) In-Reply-To: <9308251613.AA09340@cormorant.cl.cam.ac.uk> from "Mike.Gordon@cl.cam.ac.uk" at Aug 25, 93 05:13:01 pm X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 878 Mike.Gordon@cl.cam.ac.uk has said: > I think ADD_CONV -- or something like it -- is hard coded in > ICL's ProofPower. They did some experiments to find the minimal hard coding > to get good efficiency. That's what I've heard ... certainly it allows them to rewrite "FACT 10" seemingly instantaneously. Once you've got ADD_CONV, the other arithmetic conversions can be written to use it and, unlike the "proper" ADD_CONV which is O(n), most of the others can use divide and conquer techniques to yield O(log n) performance. -------------------------------------------------------------------------- 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