Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <27563-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 23:30:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06669; Wed, 8 Jul 92 15:17:47 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06664; Wed, 8 Jul 92 15:17:39 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <27434-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 23:14:07 +0100 To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: What is $# in the HOL logic? In-Reply-To: Your message of Wed, 08 Jul 92 14:35:08 -0700. <9207082135.AA02819@maui.cs.ucla.edu> Date: Wed, 08 Jul 92 23:14:02 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.436:08.06.92.22.14.10"@cl.cam.ac.uk> > I tried to define $# in the HOL logic to parallel the $# in ML, > but found out that there was already a constant named `#`. > What does $# mean? Strangely, the type of $#, ":word0", is not a type! You've just discovered one of the vestiges of some hardware-specific tools in HOL, namely classes of constants that denote bit-vectors. The built-in parser is set up to accept these constants even before their types have been defined. For example, `#11001100` is the name of what would be a constant of type :word8 representing a bit vector of length 8. When the parser sees "#11001100" it tries to create the corresponding constant of type :word8 (and it erroneously succeeds). Presumably "#" is then a :word0! You should really get an error message if you type in one of these constants when the corresponding :wordN type is not yet defined (something like strings). Alternatively (and better) we need a way of having library-loaded parser extensions... Tom PS: the :wordn types and the constants #xxxxx are used by Wai Wong's development of the bit vector library.