Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sat, 20 Mar 1993 18:52:35 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06786; Sat, 20 Mar 93 10:32:10 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Moby.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06781; Sat, 20 Mar 93 10:31:58 -0800 Received: by makaha.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA17586; Sat, 20 Mar 93 10:31:47 -0800 Date: Sat, 20 Mar 93 10:31:47 -0800 From: toal@edu.ucla.cs (Ray J. Toal) Message-Id: <9303201831.AA17586@makaha.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Subject: HOL said "please report it" Hi, Here's a transcript with a "please report it" error message; all I tried to do was load the `arith` library. But other libraries can be loaded .... moby 10 % hol =============================================================================== HOL88 Version 2.01 (SUN4/AKCL), built on 9/3/93 =============================================================================== #let test = ETA_AX;; test = |- !t. (\x. t x) = t #load_library `arith`;; Loading library arith ... Loading library reduce ... Extending help search path. Loading boolean conversions........ Loading arithmetic conversions.................. Loading general conversions, rule and tactic..... Library reduce loaded. .Updating help search path .......................................................................................................................................................................... Error in HOL system, please report it. (Diagnostic: PRIMVAL) Error in HOL system, please report it. (Diagnostic: PRIMVAL) ill-typed phrase: (\Max_bound.(\bl.if ((Numerator r)<0) then (Min_bound ((map (SIMP_mult r)) bl)) else (Max_bound ((map (SIMP_mult r)) bl)))) has an instance of type ((bound list -> bound) -> * list -> bound) which should match type (((rat # (* # rat) list) -> **) -> (rat # (* # rat) list) -> **) ill-typed phrase: (\Min_bound.(\bl.if ((Numerator r)<0) then (Max_bound ((map (SIMP_mult r)) bl)) else (Min_bound ((map (SIMP_mult r)) bl)))) has an instance of type ((bound list -> bound) -> * list -> bound) which should match type (((rat # (* # rat) list) -> **) -> (rat # (* # rat) list) -> **) ill-typed phrase: (\Pos_inf.if ((Numerator r)<0) then Neg_inf else Pos_inf) has an instance of type (bound -> bound) which should match type (((rat # (* # rat) list) -> **) -> (rat # (* # rat) list) -> **) ill-typed phrase: (\Neg_inf.if ((Numerator r)<0) then Pos_inf else Neg_inf) has an instance of type (bound -> bound) which should match type (((rat # (* # rat) list) -> **) -> (rat # (* # rat) list) -> **) 4 errors in typing typecheck failed evaluation failed load -- /s/local2/hol/Library/arith/sup-inf evaluation failed load -- /s/local2/hol/Library/arith/arith #load_library `ind_defs`;; Loading library ind_defs ... ............................................................... Library ind_defs loaded. () : void =========================================================================== I suppose something is wrong with our "system" because it loaded fine last week. By the way I did not know who at cl.cam.ac.uk to send this to so I sent it to info-hol. Who *should* such messages be sent to? Thanks Ray