Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <18173-0@swan.cl.cam.ac.uk>; Fri, 17 Jan 1992 13:18:50 +0000 Received: by ted.cs.uidaho.edu. (16.6/1.34) id AA27628; Fri, 17 Jan 92 05:09:21 -0800 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 AA27624; Fri, 17 Jan 92 05:09:16 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <18023-0@swan.cl.cam.ac.uk>; Fri, 17 Jan 1992 13:10:48 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: Re: Why sets? Date: Fri, 17 Jan 92 13:10:44 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.032:17.00.92.13.10.57"@cl.cam.ac.uk> > Incidentally, I intend to rewrite pred_sets to make it parallel > the library sets, which is the most developed of the set theory > libraries. If anyone strongly objects to this, please post me > as soon as possible, as I intend to do this soon. This has, in fact, turned out to be trivial. The sets library (in version 2) is developed on the basis of only two "primitive" theorems derived from the type definition. Rederiving them for *->bool instead of (*)set was easy, and the remainder of the library just built for sets-as-predicates with few changes required. The point of this post is to ask if anyone uses the theorems about the properties of functions expressed in pred_sets by the constants: -->, -->>, >-->, <-->, ...etc If so, then I suppose this stuff from pred_sets will have to be rewritten, not to mention incorporated into the sets library as well. Tom