Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Tue, 12 Jan 1993 15:23:12 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22519; Tue, 12 Jan 93 07:11:36 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA22514; Tue, 12 Jan 93 07:11:22 -0800 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA13903; Tue, 12 Jan 93 10:13:01 -0500 Message-Id: <9301121513.AA13903@air52.larc.nasa.gov> Date: Tue, 12 Jan 93 10:13:01 -0500 From: Victor "A." Carreno To: chou@edu.ucla.cs, slind@de.tu-muenchen.informatik Subject: Re: BETA_CONV In-Reply-To: Mail from 'chou@cs.ucla.edu' dated: Tue, 12 Jan 93 00:34:53 PST Cc: info-hol@edu.uidaho.cs.ted Ching Tsun writes: > Good point, I didn't notice this until you mention it. > No, I did not use any sticky type. However, in > "(\i j. (\i j. i > j))" > HOL88 apparently assumes the first i and j are of type :num > because the second i and j are. However, > "(\i' j'. (\i j. i > j))" > does not parse. Yet another peculiarity of HOL88. I was puzzled by this for a while from a Roger Jones posting. The explanation is in DESCRIPTION section 11.4. ** "HOL types and terms can be input to the system in two ways: by using constructor functions, or by using quotations. The former allows some terms to be built which cannot be constructed using quotation. For example, a term containing two variables with the same name but different types, [ ... ], can be built only by using constructors. [ ... ] ... since the type checker uses the heuristics that all variables in a term with the same name have the same type." ** If this heuristic was not used then the term "\x.x+1" could be i) \x:num.x+1 ii) \x:bool.x+1 iii) \x:*.x+1 etc. making it a real pain to write any term. Victor.