Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Wed, 9 Sep 1992 01:54:03 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18208;
          Tue, 8 Sep 92 17:40:57 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from dubhe.anu.edu.au by ted.cs.uidaho.edu (16.6/1.34) id AA18203;
          Tue, 8 Sep 92 17:40:39 -0700
Received: from enif.anu.edu.au by cs.anu.edu.au (4.1/SMI-4.0) id AA23235;
          Wed, 9 Sep 92 10:39:08 EST
Date: Wed, 9 Sep 92 10:39:07 EST
From: rachel@au.edu.anu.dubhe (Rachel Onate)
Message-Id: <9209090039.AA23235@cs.anu.edu.au>
To: info-hol@edu.uidaho.cs.ted
Subject: new_recursive_definition question



I would like to know how the new_recursive_definition was implemented 
with respect to a user's partial specification of a value of a function 
defined on a concrete type, by allowing defining equations for some of 
the constructors to be omitted.  The example given in the HOL System 
description manual (1988, p179) was the definition of "Label" of the 
leaves of the tree:

#let Label =
# new_recursive_definition false btree_Axiom `Label`
#  "Label (LEAF (x:*)) = x";;
Label = |- !x. Label (LEAF x) = x

Here, an internal node does not have label, so it was left unspecified.

More questions:
(1) Doesn't HOL implement total functions only?
(2) What happens if a user try to access "Label (Node t1 t2)"?

Thanks.

Rachel
rachel@cs.anu.edu.au
Department of Computer Science
Australian National University
GPO Box 4