Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <11510-0@swan.cl.cam.ac.uk>; Tue, 28 Jul 1992 10:45:53 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22832;
          Tue, 28 Jul 92 02:08:47 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA22827;
          Tue, 28 Jul 92 02:08:39 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <10703-0@swan.cl.cam.ac.uk>;
          Tue, 28 Jul 1992 09:58:03 +0100
To: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Cc: info-hol@edu.uidaho.cs.ted (HOL Mailing List), Tom.Melham@uk.ac.cam.cl
Subject: Re: Set parsing?
In-Reply-To: Your message of Mon, 27 Jul 92 14:45:35 -0700. <9207272145.AA14503@leopard.cs.uidaho.edu>
Date: Tue, 28 Jul 92 09:57:57 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.705:28.06.92.08.58.06"@cl.cam.ac.uk>


> I want to define a function which takes a number (Num)
> and returns the set of all pairs of numbers in which the
> first number is Num, and the second is less than the first.
> 
> "foo Num = {(Num, i) | i < Num}"
> 
> gets parsed to 
> 
> "foo Num = GSPEC (\(Num, i). ((Num, i),i < Num))"
> 
> Which is actually the set of all pairs in which the second number
> is less than the first number.
> 
> Typing in a GSPEC directly
> 
> "foo Num = GSPEC (\i. ((Num, i), i < Num))"
> 
> causes the pretty-printer to not recognize it as set notation.

The behaviour you describe is due to a deliberate decision we made 
concerning the parsing/printing of the set notation {E | P}.  The
rule (taken from the version 2.01 sets library manual) is

   "... a quotation of the form "{E | P}" parses to:

            GSPEC (\x1...xn.(E,P))

    where x1, ..., xn are the variables that occur free in both
    the expression E and the proposition P (i.e. the set {x1,...,xn}
    is the intersection of the set of free variables of E and the set 
    of free variables of P).  If there are no variables free in both 
    E and P, then a parser error is generated. ..."

Moreover, the pretty-printer prints only generalized set abstractions
that could also be parsed.  Unfortunately, this means that the notation
will sometimes not behave as intended---for example, as above.  However,
we played with the alternatives for a long time, and I believe that what
we have is a good compromise.  

For the specific case mentioned above, Jim Alves-Foss's solution

> foo num = {(n,i) | (n = num) /\ (i < num)}

is a good one.

Tom