Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Wed, 24 Nov 93 12:08:57 +0100
From: vdvoort@cs.utwente.nl (Mark van de Voort)
Message-Id: <9311241108.AA16632@perseus.cs.utwente.nl>
To: info-hol@cs.uidaho.edu
Subject: Re: Need "an undefined value", but not what you think.
In-Reply-To: Mail from 'shaw@cs.ucdavis.edu (Rob Shaw)' dated: Tue, 23 Nov 1993 23:07:07 -0800

Rob Shaw asked:

RS> But I can't just define myEL to be 
RS> something like
RS> 
RS> myEL i l = (i in bounds) => (EL i l) | UNDEF
RS>
RS> because UNDEF = UNDEF, which is not what I want. Is there any way
RS> for me to define lists such that (EL 9 [1;2;3]) can be proved
RS> neither equal nor unequal to any term that is not (EL 9 [1;2;3]) ??

Maybe you want to define myEL to be:

myEL i l = (i in bounds) => (EL i l) | (UNDEF i l)

that is, you tag the value UNDEF with both the index and the list.

I have one little question: why do you want EL 10 [0;1;2;3] to be different 
from EL 9 [1;2;3]? I would think that they are equal since a series of
reduction-steps exists which reduce both to the same form (i.e. EL 9 [1;2;3]).

Mark.