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; Wed, 25 Aug 1993 20:00:22 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02741; Wed, 25 Aug 93 11:46:25 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from laforge.cs.byu.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA02737; Wed, 25 Aug 93 11:46:08 -0700 Received: by laforge (5.65/DEC-Ultrix/4.3) id AA16993; Wed, 25 Aug 1993 12:45:23 -0600 Message-Id: <9308251845.AA16993@laforge> To: info-hol@dworshak.cs.uidaho.edu Cc: "Tim Leonard, DTN 225-5809, HLO2-3/C11" Subject: Re: numerals by pretty printer instead by num_CONV? In-Reply-To: Your message of Wed, 25 Aug 93 14:32:10 -0400. <9308251831.AA01276@easynet.crl.dec.com> Date: Wed, 25 Aug 93 12:45:22 -0600 From: Phil Windley X-Mts: smtp On Wed, 25 Aug 93 14:32:10 EDT, leonard@ricks.enet.dec.com wrote: +------------ | I will assume that the parser should accept the second form and produce the | first, and the pretty-printer should accept the first and produce the second, | and that hol will not generally support other representations, but other (rea | "worse") arrangements are possible, and you may want to think about it before | accepting the assumption. I fully support Tim's position and his suggestions. Years ago, I did something less general than Tim's library to represent and reason about decimal numbers in HOL rather than the standard unary representation. Simply put, this library made the microprocessor proof I did for my dissertation possible. I was not doing anything nearly as demanding as reasoning about 64 bit numbers, but even the unary representation was just not enough. --phil--