Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 2 Dec 1992 10:43:40 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13662; Wed, 2 Dec 92 02:22:05 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13657; Wed, 2 Dec 92 02:21:48 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Wed, 2 Dec 1992 10:20:46 +0000 To: blok@nl.utwente.cs (Rintcius Blok) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: recursive def. problem In-Reply-To: Your message of Tue, 01 Dec 92 17:37:05 +0100. <9212011637.AA07134@apollo.cs.utwente.nl> Date: Wed, 02 Dec 92 10:20:40 +0000 From: Tom Melham Message-Id: <"nene.cl.ca.944:02.12.92.10.20.47"@cl.cam.ac.uk> > > I have a problem with defining a simple looking function. I just > > want to write a recursive function based on the type (*)ltree, > > that returns the root of a ltree. > > I tried the following definition: > > > > #new_recursive_definition false ltree_Axiom > > # `GetTop` > > # "GetTop (Node (top:*) desc) = top";; > > I think the problem arises because |ltree_Axiom|, involving as it > does the MAPping of the function over a list of subtrees, is not > quite of the form expected by |new_recursive_definition|: Precisely. The function new_recursive_definition is expects recursion theorems *of the form proved by define_type*. And ltree_Axiom is not one of those. Tom