Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <17124-0@swan.cl.cam.ac.uk>; Mon, 15 Jun 1992 16:27:16 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13701; Mon, 15 Jun 92 08:13:18 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA13646; Mon, 15 Jun 92 08:13:14 -0700 Received: from localhost by panther.cs.uidaho.edu with SMTP id AA18674 (5.65c/IDA-1.4.4 for info-hol@cs.uidaho.edu); Mon, 15 Jun 1992 08:19:01 -0700 Message-Id: <199206151519.AA18674@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: [Wishnu Prasetya: bad varstruct??] Date: Mon, 15 Jun 92 08:19:00 -0700 From: Phil Windley X-Mts: smtp [ This was sent to info-hol-request. I presume the author meant to send it to info-hol instead - PJW ] From: Wishnu Prasetya Message-Id: <199206151439.AA26563@infix.cs.ruu.nl> Subject: bad varstruct?? To: info-hol-request@ted.cs.uidaho.edu (hol mailing list) Date: Mon, 15 Jun 92 16:39:40 METDST X-Mailer: ELM [version 2.3 PL11] Hi, I'm a novice in HOL and got the following problem, which perhaps someone can help. 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? I'm aware that HOL may require an explicit type instantiation to resolve its evaluation, but the definition above seems to be explicit enough, doesn't it? I would certainly be thankful if someone cares to help me in this. Thank you, Wishnu Prasetya CS, Utrecht Univeristy, Holland.