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; Fri, 28 Oct 1994 04:13:21 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA11688;
          Thu, 27 Oct 1994 22:00:59 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA11684;
          Thu, 27 Oct 1994 22:00:50 -0600
Received: from toadflax.cs.ucdavis.edu (toadflax.cs.ucdavis.edu [128.120.56.188]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id UAA00976 
          for <info-hol@cs.uidaho.edu>; Thu, 27 Oct 1994 20:52:56 -0700
Received: from ice.cs.ucdavis.edu by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.6) 
          id AA16724; Thu, 27 Oct 94 20:52:47 PDT
Received: by ice.cs.ucdavis.edu (5.65/UCD.CS.2.6) id AA06135;
          Thu, 27 Oct 1994 20:52:45 -0700
Date: Thu, 27 Oct 1994 20:52:45 -0700
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9410280352.AA06135@ice.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: Quick Theoretical Question


Hi all,

I know I could look this up, but it's short and I'm likely to get a better
answer from the members of this list anyway.

Briefly, are the consistency of HOL and the disallowance of partial 
functions related? Suppose I were allowed to define a function over
only two of the three constructors for a type, leaving other members of
the type "undefined". If there is a consistency problem, how does this
function definition cause it?

Thanx,

Rob