Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 15 Mar 1994 17:53:55 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA07253;
          Tue, 15 Mar 1994 10:24:40 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from puma.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA07249;
          Tue, 15 Mar 1994 10:24:39 -0700
Received: from localhost by puma.cs.byu.edu (1.38.193.4/CS-Client) id AA03618;
          Tue, 15 Mar 1994 10:27:37 -0700
Message-Id: <9403151727.AA03618@puma.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: literals
Date: Tue, 15 Mar 1994 10:27:36 -0700
From: Phil Windley <windley@lal.cs.byu.edu>



Does anyone have a good way of checking for literals in HOL88?

I'd like this:

let tm = mk_const('a',":num");;

is_lit "5";;  ==> true

is_lit "T";;  ==> true

is_lit tm;; ==> false

Of copurse, I can write a funtion that approximates this for bools, nums,
etc, but I was wondering if theres a syntactic identifier for literals.

--phil--