Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 26 May 1995 06:14:55 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA294213537; Thu, 25 May 1995 22:45:37 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from vega.anu.edu.au by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA294183535; Thu, 25 May 1995 22:45:35 -0600 Received: (from mcn@localhost) by vega.anu.edu.au (8.6.12/8.6.9) id OAA18669 for info-hol@leopard.cs.byu.edu; Fri, 26 May 1995 14:27:19 +1000 Date: Fri, 26 May 1995 14:27:19 +1000 From: Malcolm Newey Message-Id: <199505260427.OAA18669@vega.anu.edu.au> To: info-hol@leopard.cs.byu.edu Subject: Re: Curry and uncurry X-Sun-Charset: US-ASCII Ray Toal says: > Of course you do not *need* the type pair at all in Type Theory. > It is not primitive. Probably what you could say is that > pairs do not exist and that f(a,b) is just syntactic sugar > for f a b. Indeed. ... and that was how it was done in a HOL ancestor - Stanford LCF.