Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <00268-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 22:52:13 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22102; Mon, 27 Jul 92 14:42:13 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA22047; Mon, 27 Jul 92 14:42:08 -0700 Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA14503; Mon, 27 Jul 92 14:45:36 -0700 From: weiss@edu.uidaho.cs.leopard (Phil Weiss) Message-Id: <9207272145.AA14503@leopard.cs.uidaho.edu> Subject: Set parsing? To: info-hol@edu.uidaho.cs.ted (HOL Mailing List) Date: Mon, 27 Jul 92 14:45:35 PDT Mailer: Elm [revision: 66.33] 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