Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9208092216.AA01483@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Questions about define_type
Date: Sun, 09 Aug 92 15:16:29 PDT
From: chou@edu.ucla.cs

The following is quoted from the manual page of define_type:

  The type specification given as the second argument to define_type must be a
  string of the form:
  
     `op = C1 ty ... ty | C2 ty ... ty | ... | Cn ty ... ty`
  
  where op is the name of the type constant or type operator to be
  defined, C1, ..., Cn are identifiers, and each ty is either a (logical)
  type expression valid in the current theory (in which case ty must not
  contain op) or just the identifier `op' itself.


Why can't ty be a type expression like (op)list or *->op ?
Is there a hack to get around this problem?

More specifically, I'd like to define the syntax of a toy "programming
language", one of whose constructs is something like:

  `statement = ...
	     | CHOOSE (* -> statement)

That is, CHOOSE takes a family of statements, represented by a function
of type * -> statement, and returns a single statement.  Of course, 
I could have followed Tom Melham's work on pi-calculus and formalize 
the notion of abstraction in the syntax, but that seems an over-kill 
for the simple application I have in mind.

By the way, can any of the constructors (C1, C2, etc.) be made into 
infixes or binders?

- Ching Tsun