Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: jimaf@edu.uidaho.cs.leopard (Jim Alves-Foss)
Message-Id: <9207272322.AA14615@leopard.cs.uidaho.edu>
Subject: Re: Set parsing?
To: weiss@edu.uidaho.cs.leopard (Phil Weiss) (Phil Weiss)
Date: Mon, 27 Jul 92 16:22:43 PDT
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: <9207272145.AA14503@leopard.cs.uidaho.edu>; from "Phil Weiss" at Jul 27, 92 2:45 pm
Mailer: Elm [revision: 66.33]

Phil writes:
> 
> 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.
> 
> Is the last definition of foo what I really want?  How should I
> really go about this?
> 
> Phil.
> --
> Philip Weiss	Laboratory for Applied Logic	weiss@leopard.cs.uidaho.edu
> (Disclaimer: My views are not their views)	weiss872@snake.cs.uidaho.edu
> 

Try the following:

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

-Jim Alves-Foss
 Assistant Professor
 Computer Science Department                (208) 885-7232
 University of Idaho                        (jimaf@leopard.cs.uidaho.edu)