Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Mon, 5 Oct 1992 15:38:54 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19971;
          Mon, 5 Oct 92 07:20:38 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA19966;
          Mon, 5 Oct 92 07:20:16 -0700
Received: by infix.cs.ruu.nl id AA24627 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Mon, 5 Oct 1992 15:19:14 +0100
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199210051419.AA24627@infix.cs.ruu.nl>
Subject: QUESTION: unbound type variable in new_definition
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Mon, 5 Oct 92 15:19:12 MET
X-Mailer: ELM [version 2.3 PL11]

Hi there!

I try to define DISJ_REL (disjunctive relation) as follows:

  let DISJ_REL = new_definition
    (`DISJ_REL`,
    "DISJ_REL (R:(*->bool)->(*->bool)->bool) =
    !p (W:**->(*->bool)). (!i:**. R (W i) p) ==> R (\s:*. ?i. W i s) p") ;;

but this is of no success. I get the following error:
  
  evaluation failed     ** an unbound type variable in definition

which I don't really understand why. The closer hint I gather from the
referrence is that applying new_definition to OP x y = t may fail if
there is a type in x, y, or t that does not occur in OP. But this
doesn't seem the case here. Also:

  let DISJ_REL = new_definition
    (`DISJ_REL`,
    "DISJ_REL (R:(*->bool)->(*->bool)->bool) =
     !p (W:num->(*->bool)). (!i:num. R (W i) p) ==> R (\s:*. ?i. W i s) p") ;;

which is the same as the first except that I have replaced ** for num.
Above does not give any problem, though.

Any one want ot comment on this? Is ** not allowed because such may
give contradiction?

Thank you kindly,


Wishnu Prasetya
  


--