Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 10:30:59 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02187;
          Wed, 24 Nov 1993 03:20:50 -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 AA02183;
          Wed, 24 Nov 1993 03:20:45 -0700
Received: from sirius.brunel.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA06568; Wed, 24 Nov 93 02:18:07 -0800
Received: from elektra.brunel.ac.uk by sirius.brunel.ac.uk with SMTP (PP) 
          id <17099-0@sirius.brunel.ac.uk>; Wed, 24 Nov 1993 10:17:43 +0000
From: Simon Finn <simon@ahl.co.uk>
Received: from Delta.ahl.co.uk by Pinky.ahl.co.uk; Wed, 24 Nov 93 10:24:09 GMT
Date: Wed, 24 Nov 93 10:24:07 GMT
Message-Id: <179.9311241024@Delta.ahl.co.uk>
To: shaw@cs.ucdavis.edu
Subject: Re: Need "an undefined value", but not what you think.
Cc: info-hol@cs.uidaho.edu


Rob Shaw says:

>  I want
> to eventually work with a version of lists such that indexing 
> beyond the end of one is "an undefined value" in the way that
> 12/0 is "an undefined value".

In LAMBDA, you could write:

    fun EL   0 (h:t) = h
      | EL 1'n (h:t) = EL n t;

In HOL, you need to define EL to be a term something like the following:

    @f. (!h t.   f 0 (CONS h t) = h)
     /\ (!h t n. n < length t -> f (SUC n) (CONS h t) = f n t)


Simon Finn (Abstract Hardware Ltd.)