Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 13 Jun 1994 22:07:50 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25192; Mon, 13 Jun 1994 15:07:16 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25187; Mon, 13 Jun 1994 15:07:09 -0600 Received: by crl.dec.com; id AA25168; Mon, 13 Jun 94 16:48:47 -0400 Received: by easynet.crl.dec.com; id AA23428; Mon, 13 Jun 94 16:48:45 -0400 Message-Id: <9406132048.AA23428@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Mon, 13 Jun 94 16:48:47 EDT Date: Mon, 13 Jun 94 16:48:47 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 13-Jun-1994 1541" To: hol2000@leopard.cs.byu.edu Apparently-To: hol2000@leopard.cs.byu.edu Subject: Re: pretty printing versus mk_const Ralf Reetz suggests that strings and nums could be better represented with lists, and Phil Windley asks how I did hex constants. My numeral library represents numerals using lists, which does eliminate the need for num_CONV and its associated mk_thm. A decimal numeral is represented by something like this: DECIMAL [2;4;7;5] and the library supports arithmetic on such things. You only need a constant for each of the digits in the largest-supported radix. The parser and pretty printer can make this look pretty, if you want (at least for decimal --- other radices won't be as pretty). The parser, pretty printer, and the numeral library arithmetic support are the only users of the constants, so it doesn't matter if they're ugly, like DIGIT_0 and DIGIT_15.