Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Sun, 13 Jun 93 15:17:10 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9306132217.AA19285@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: term parsing and ->


I have a novice question about term parsing and ->. First, if I
try to parse a polymorphic term, I get an error, as expected:
|  
|  "APPEND";;
|  
Gives:
|  
|  Indeterminate types:  "APPEND:(?1)list -> ((?1)list -> (?1)list)"
|  
|  evaluation failed     types indeterminate in quotation
|  
Fine. Also as expected, if I give enough info to allow the type 
inference to succede, it does so:
|  
|  "APPEND (ls1:((num)list))";;
|  
Gives:
|  
|  "APPEND ls1" : term
|  
But the next example will fail, and I don't know why.
|  
|  "APPEND:(((num)list)->((num)list))->(num)list";;
|  
Gives:
|
|  evaluation failed     types in quotation
|
I find this message contradictory. It seems to allude that type
expressions are not allowed inside double quotes -- a false 
allusion, as the previous example contained :((num)list) inside
double quotes. I must assume it is the -> that is causing the 
trouble. Questions:

(1) May -> ever appear inside a type expression inside double
    quotes? When and why? 

(2) If not (1), then why is a type operator, such as "list" 
    allowed, but not -> ?

(3) Where in the manuals should I have looked to find the answers?
    Sections 11.3 and 11.4 lead me to believe that, as long as
    no type is indeterminate, "constant:type-expr" is legal. The
    table in 11.4.2 makes no restrictions on the allowed forms
    of the little sigma.

Many thanx to anyone who can reconcile the behaviour in the
three examples above!

Rob Shaw