Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Tue, 23 Mar 1993 15:32:53 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11860;
          Tue, 23 Mar 93 07:11:09 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA11855;
          Tue, 23 Mar 93 07:10:29 -0800
Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) 
          id AA06146; Tue, 23 Mar 93 10:10:03 EST
Date: Tue, 23 Mar 93 10:09:58 EST
From: shb@com.oracorp
Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA01288;
          Tue, 23 Mar 93 10:09:58 EST
Message-Id: <9303231509.AA01288@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Uncurried hol90.5 define_type constructors

I sent this note out earlier, but haven't seen it yet on our local rn
version of info-hol, so there might be a problem.  I've also added
another question.

Is there any way to get the hol90.5 version of define_type to define a
concrete recursive type with a constructor whose argument type is a
pair or other tuple?  In hol 88 one says "foo num num" to get a Curried
constructor, and says "foo num#num" to get an un-Curried one.  In
hol90.5, "foo of num # num" and "foo of (num # num)" both give a
Curried constructor.

Also, if it is possible to define non-Curried constructors in hol90.5,
can they take as arguments the type being defined?  That wasn't
possible under hol88 2.0.

Steve Brackin
ORA