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; Wed, 25 May 1994 14:08:50 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA13711; Wed, 25 May 1994 07:06:23 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA13707; Wed, 25 May 1994 07:06:21 -0600 Received: by crl.dec.com; id AA26807; Wed, 25 May 94 09:02:17 -0400 Received: by easynet.crl.dec.com; id AA12415; Wed, 25 May 94 09:02:16 -0400 Message-Id: <9405251302.AA12415@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Wed, 25 May 94 09:02:16 EDT Date: Wed, 25 May 94 09:02:16 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 25-May-1994 0857" To: hol2000@leopard.cs.byu.edu Apparently-To: hol2000@leopard.cs.byu.edu Subject: Pattern matching in lambda abstraction Richard Boulton writes: > Having said that, there is a strong case for making abstractions over tuples > built-in. In fact, is there any reason why such a construct can't subsume the > existing ABS, it being taken as the special case in which the tuple has one > component? and Konrad Slind replies: > Maybe we should go further and provide for ML-style patterns in HOL > lambda abstractions. The problem is what to do with unmatched patterns: What's the problem? Don't allow unmatched patterns. Tim