Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <27179-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 22:47:47 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06447;
          Wed, 8 Jul 92 14:34:27 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06442;
          Wed, 8 Jul 92 14:34:14 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61c+YP/3.19) id AA02819;
          Wed, 8 Jul 92 14:35:10 -0700
Message-Id: <9207082135.AA02819@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: What is $# in the HOL logic?
Date: Wed, 08 Jul 92 14:35:08 PDT
From: chou@edu.ucla.cs

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!

#is_constant `#` ;;
true : bool

#type_of "$#" ;;
":word0" : type

#dest_type it ;;
(`word0`, []) : (string # type list)

#":word0" ;;
evaluation failed     mk_type in quotation

#is_type `word0` ;;
false : bool


- Ching Tsun