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; Mon, 15 May 1995 17:33:07 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA189644272; Mon, 15 May 1995 10:11:12 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA189574254; Mon, 15 May 1995 10:10:54 -0600 Received: from woodcock.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 15 May 1995 17:09:34 +0100 X-Mailer: exmh version 1.5.2 12/21/94 To: info-hol@leopard.cs.byu.edu Subject: Re: Sequences In-Reply-To: Your message of "Mon, 15 May 1995 09:25:36 MDT." <"swan.cl.cam.:260760:950515155144"@cl.cam.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Mon, 15 May 1995 17:09:28 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:271800:950515160937"@cl.cam.ac.uk> Given we have finite lists and infinite sequences in HOL already, can't one base a new type (*)seq by the simple disjoint union: (*)seq = FINITE ((*)list) | INFINITE (num -> *) Then all operations and constants such as "EL", "HD", "TL", "NIL", "LENGTH", "IS_FINITE" and so on have obvious logical definitions by cases, e.g. seq_EL n (FINITE l) = EL n l seq_EL n (INFINITE f) = f n seq_HD n (FINITE l) = HD l seq_HD n (INFINITE f) = f 0 etc. etc. This seems adequate to me, though I'm willing to be enlightened. Don Syme