Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Questions about define_type
In-Reply-To: Your message of Sun, 09 Aug 92 15:16:29 -0700. <9208092216.AA01483@maui.cs.ucla.edu>
Date: Mon, 10 Aug 92 08:13:12 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.912:10.07.92.07.13.30"@cl.cam.ac.uk>


chou@edu.ucla.cs writes:

> 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 ?

Solving the equation with ty being (op)list or *->op requires more logical
infrastructure than is presently there.  There is no reason in principle
why this couldn't be done; but one has to stop programming *somewhere*,
and when creating define_type I stopped where the manual says. Note 
however that ty=op->* is of course not possible.

>Is there a hack to get around this problem?

For (op)list you can use the underlying type (*)ltree --- see my
paper on the types package for hints.  For *->op you'll have to do
more work by hand.

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

No, but this should really be changed someday.

Tom