Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <18282-0@swan.cl.cam.ac.uk>; Mon, 15 Jun 1992 17:08:33 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13780; Mon, 15 Jun 92 08:47:04 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13775; Mon, 15 Jun 92 08:46:51 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <17734-0@swan.cl.cam.ac.uk>; Mon, 15 Jun 1992 16:44:04 +0100 To: wishnu@nl.ruu.cs Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: [Wishnu Prasetya: bad varstruct??] In-Reply-To: Your message of Mon, 15 Jun 92 08:19:00 -0700. <199206151519.AA18674@panther.cs.uidaho.edu> Date: Mon, 15 Jun 92 16:43:55 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.737:15.05.92.15.44.12"@cl.cam.ac.uk> Regarding: > I'm trying to define a simple function called root, which given an > ltree of something, will return the root of the tree. Here is how I > have coded my definition: > > new_definition(`root_def`, > "(root:((*)ltree->*)) (Node a t) = a") ;; > > but then I got an error saying > > evaluation failed bad varstruct > > What's that supposed to mean? What was wrong with my definition? The function new_definition works only for definitions of a specific form, namely: fun v1 v2 ... vn = term where v1,v2,...,vn are either variables or tuples of variables (the latter are called "varstructs"). Your definition has the form: root (Node a t) = t and "Node a t" is NOT a varstruct. See the REFERENCE manual for more details. By the way, you can define your root function as follows: let th1 = theorem `ltree` `ltree_Axiom` in let th2 = ISPEC "\x:(*)list.\v:*.\tl:((*)ltree)list.v" th1 in let th3 = EXISTENCE (BETA_RULE th2) in new_specification `root_DEF` [`constant`,`root`] th3;; > I would certainly be thankful if someone cares to help me in this. No problem, Tom