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; Tue, 25 Apr 1995 21:35:55 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA150598853;
          Tue, 25 Apr 1995 13:40:53 -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 AA150058792;
          Tue, 25 Apr 1995 13:39:52 -0600
Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl;
          Tue, 25 Apr 1995 20:09:30 +0100
X-Mailer: exmh version 1.5.2 12/21/94
To: info-hol@leopard.cs.byu.edu
Subject: A trivial "option" library
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 25 Apr 1995 20:09:27 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:138520:950425190942"@cl.cam.ac.uk>


I've been thinking that a (trivial) "option" library should be included
with HOL.  This would just be the type

	option = SOME of 'a | NONE

This type or its logical equivalent (I think Elsa called it "lift")
has cropped up from time to time in different applications, and
seems to be among the class of trivial types like sums and pairs
that just should be there.  

I'll write the code and documentation tomorrow (for both HOLs), so
if anyone has opinions about this I'd like to hear.  I think the only 
constants besides SOME and NONE I will include will be IS_SOME and
IS_NONE.

Donald