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:18:53 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02394; Wed, 24 Nov 1993 04:34:39 -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 AA02390; Wed, 24 Nov 1993 04:33:37 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA06598; Wed, 24 Nov 93 03:31:22 -0800 Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 24 Nov 1993 11:30:48 +0000 To: David Shepherd Cc: shaw@cs.ucdavis.edu (Rob Shaw), info-hol@cs.uidaho.edu (info-hol mailing list), Paul.Curzon@cl.cam.ac.uk Subject: Re: Need "an undefined value", but not what you think. In-Reply-To: Your message of "Wed, 24 Nov 93 10:46:00 GMT." <1410.9311241046@frogland.inmos.co.uk> Date: Wed, 24 Nov 93 11:30:26 +0000 From: Paul Curzon Message-Id: <"swan.cl.cam.:057860:931124113057"@cl.cam.ac.uk> Ooops: a correction to what I just said >|- F ==> (WOMBAT 9 [1;2;3] = EL 9 [1;2;3]) > >|- F ==> (WOMBAT 8 [2;3] = EL 8 [2;3]) > >ie >|- (WOMBAT 9 [1;2;3] ~= EL 9 [1;2;3]) >|- (WOMBAT 8 [2;3] ~= EL 8 [2;3]) The above step does not follow. You actually dont know anything about WOMBAT in this case. >For EL what needs to be done is instead of (in HOL90 syntax) the >definition: > >val EL = new_recursive_definition > {name = "EL", > fixity = Prefix, > rec_axiom = num_Axiom, > def = --`(!l. EL 0 l = (HD l:'a)) /\ > (!l:'a list. !n. EL (SUC n) l = EL n (TL l))`--}; How does this help in the example given? You still have the clause: EL (SUC n) l = EL n (TL l)) so EL 10 [0;1;2;3] = EL (SUC 9) [0;1;2;3] = EL 9 (TL [0;1;2;3]) = EL 9 [1;2;3]