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, 24 Nov 1993 13:41:10 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02749; Wed, 24 Nov 1993 06:36:33 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA02745; Wed, 24 Nov 1993 06:36:32 -0700 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA06662; Wed, 24 Nov 93 05:34:13 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Wed, 24 Nov 1993 13:34:03 GMT From: David Shepherd Message-Id: <1955.9311241332@frogland.inmos.co.uk> Subject: Re: Need "an undefined value", but not what you think. To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Wed, 24 Nov 1993 13:32:52 +0000 (GMT) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1061 Please ignore my recent ramblings ... I was answering the wrong question! (Thanks to Brian Graham for pointing this out to me!) All my modified EL function did was to eliminate 'TL []' turning up but it doesn't in fact alter the meaning. I`d failed to see that the original desire was for |- ~(EL 10 [0,1,2,3] = EL 9 [1,2,3]) The basic problem stems from the fact that EL has a recursive definition ... i.e. EL (SUC n) is defined in terms of EL n and since it isn't really total (the HOL function is a total version of an inherently partial function) you are going to get an equality between different unknown results. So what you do need is for a precondition to the definition that you will get a "genuine" answer - which is what Paul Curzon's WOMBAT function does. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "you might think that --- I couldn't possibly comment"