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 May 1995 14:32:39 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA172539591; Wed, 24 May 1995 06:46:31 -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 AA172509589; Wed, 24 May 1995 06:46:29 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 24 May 1995 13:34:01 +0100 X-Uri: To: info-hol@leopard.cs.byu.edu Subject: Re: Finite+Infinite Sequences In-Reply-To: Your message of "Wed, 24 May 1995 11:48:20 -0000." <9505241048.17337.0@win.icl.co.uk> Date: Wed, 24 May 1995 13:33:54 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:233440:950524123405"@cl.cam.ac.uk> If one wants to allow appending of finite and infinite sequences in any order, then maybe one *should* consider allowing at least some transfinite ordinals for the domain. How about allowing all countable ordinals? Then the domains would be segments of omega_1, so you could define the set in HOL. I suggest an "obfuscated sequences" contest to come up with the most arcane characterization possible. John.