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 11:11:23 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA03495; Thu, 26 Aug 93 03:06:20 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA03491; Thu, 26 Aug 93 03:06:18 -0700 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 26 Aug 1993 11:05:59 +0100 To: Tim Leonard Cc: info-hol@dworshak.cs.uidaho.edu Subject: Re: numerals by pretty printer instead by num_CONV? In-Reply-To: Your message of "Wed, 25 Aug 93 14:32:10 EDT." <9308251831.AA01276@easynet.crl.dec.com> Date: Thu, 26 Aug 93 11:05:45 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:084460:930826100609"@cl.cam.ac.uk> > DECIMAL [1;2;3;4;5] % = 12345 % > BINARY [1;0;0;0;0] % = 16 % > HEX [15;15] % = 255 % I'm curious: Did you find having the most significant digit as the first element of the list to be advantageous? > o that hol define a small number (like 16) of numeric constants *for use > only by the numeral library, parser, and pretty-printer* One good thing about this is that the constants can be defined rather than being built in as an axiom scheme: 1 = SUC 0 2 = SUC (SUC 0) 3 = SUC (SUC (SUC 0)) etc. (upto a *finite* (and fairly small!) number) By defining the digits as fully expanded SUC forms (as above) there is no need for num_CONV. One can simply expand using these definitions. My first reaction was to define the hex digits 0,...,9,A,...,F, but realised that having A,...,F defined like this was probably a bad idea because they are likely to get used for other things. My next reaction was to only want to define the decimal digits 0,...,9 and have 10,...,15 represented in some other way, but I couldn't come up with anything clean, so perhaps it's best to define 10,...,15 as well. I guess someone might want to use a radix higher than 16 but they can always add their own definitions for 16, 17, etc. Can anyone see a flaw in this? > o The parsing and pretty-printing of numerals is now trivial (and > doesn't use mk_thm), and can stay that way even when the user-visible > language is extended to support numerals in other radices. The pretty-printing would probably be easier if one avoids defining DECIMAL, BINARY, etc., and simply use the more general function (which I assume takes the radix as an argument). Richard.