Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <16822-0@swan.cl.cam.ac.uk>; Thu, 23 Jul 1992 11:56:14 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08471; Thu, 23 Jul 92 03:45:32 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA08466; Thu, 23 Jul 92 03:45:25 -0700 Received: by infix.cs.ruu.nl id AA25520 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Thu, 23 Jul 1992 12:46:32 +0200 From: Wishnu Prasetya Message-Id: <199207231046.AA25520@infix.cs.ruu.nl> Subject: unbounded type in definition To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Thu, 23 Jul 92 12:46:31 METDST X-Mailer: ELM [version 2.3 PL11] Hello, I have the following two definitions: new_definition (`flup`, "flup X = !fP:num->*. !V:(num) set. !i:num. i IN V ==> X (fP i)") ;; new_definition (`flop`, "flop X = !fP:**->*. !V:(**) set. !i:**. i IN V ==> X (fP i)") ;; it doesn't matter what flup and flop may represent, but flup is accepted by HOL, but not flop. The only difference between flup and flop is that I have replace the type `num` in flup with the polymorphic `**` in flop. HOL doesn't accept this, complaining that ** is an unbound type. Then how do I suppose to define flop? I mean !i:**. i IN V ==> X (fP i)") as a coding for (A i: i IN V: X (fP i)) which I think is a clearly bounded quantification since V is of type `set`, which always finite. Any help? I would certainly appreciate it. Thank you kindly. -Wishnu Prasetya-