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; Fri, 28 Oct 1994 08:05:28 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA14145; Fri, 28 Oct 1994 02:00:41 -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 AA13777; Fri, 28 Oct 1994 02:00:22 -0600 Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id AAA01630 for ; Fri, 28 Oct 1994 00:51:55 -0700 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Fri, 28 Oct 1994 08:51:38 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <08725-0@i80fs2.ira.uka.de>; Fri, 28 Oct 1994 08:55:11 +0100 Date: Fri, 28 Oct 94 8:55:10 EST From: reetz To: shaw@cs.ucdavis.edu Cc: info-hol@cs.uidaho.edu Subject: Re: Quick Theoretical Question Message-Id: <"i80fs2.ira.727:28.10.94.07.55.13"@ira.uka.de> > You can, can't you? new_theory "test"; val test_axiom = define_type {fixities = [Prefix,Prefix], name = "test", type_spec= `test = test1 | test2`}; val it = |- !e0 e1. ?!fn. (fn test1 = e0) /\ (fn test2 = e1) : thm new_recursive_definition {name = "partial_fun", fixity = Prefix, rec_axiom = test_axiom, def = (--` (partial_fun test1 = F) `--)}; val it = |- partial_fun test1 = F : thm O.k. it's not really partial, it's just uncompletly defined, or let's say, it's specified. Note that --`partial_fun test2`-- does have a value but you can't prove anything about it because of lacking definition. I've never tried to prove --`partial_fun test2 = (@x.F)`-- or --`partial_fun test2 = (@x.T)`--, but that seems to be the intiutive meaning: "it is equal to some(any?) value of type test". Ralf (**************************************************************) (* *) (* Ralf Reetz *) (* *) (* University of Karlsruhe *) (* Institut fuer Rechnerentwurf und Fehlertoleranz *) (* 76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany *) (* *) (* e-mail: reetz@ira.uka.de *) (* WWW: http://goethe.ira.uka.de/people/reetz/reetz.html *) (* *) (**************************************************************)