Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 8 Jan 1994 15:35:47 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26822; Sat, 8 Jan 1994 08:31:00 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26818; Sat, 8 Jan 1994 08:30:52 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA05811; Sat, 8 Jan 1994 07:28:59 -0800 Received: from guillemot.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 8 Jan 1994 15:28:44 +0000 To: leonard@evsrv3.afl.hlo.dec.com (Tim Leonard) Cc: info-hol@cs.uidaho.edu Subject: Re: A problem in hol88 parsing "CONS ~O ops" In-Reply-To: Your message of "Wed, 29 Dec 93 19:59:41 EST." <9312300059.AA00553@evsrv3.afl.hlo.dec.com> Date: Sat, 08 Jan 94 15:28:35 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:246150:940108152854"@cl.cam.ac.uk> The parsing problem arises because |~| is treated specially, with a lower precedence than function application. Hence HOL sees "CONS ~O ops" as "CONS ~(O ops)" which explains the type error. Regarding HOL terms as akin to terms (as distinct from formulas) in first-order logic, this is what one wants. The conflation in HOL of terms and formulas, and the use of ":bool" as just another datatype, is a nice simplification, but makes it hard to get precedences `right' all the time. There is an even worse problem with |=| -- as term equality one would want to give it a higher precedence than logical connectives, but as logical equivalence one would want it lower (and it is lower). John.