Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Sun, 25 Oct 1992 22:18:54 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA27391; Sun, 25 Oct 92 13:55:16 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA27384; Sun, 25 Oct 92 13:54:46 -0800 Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0mjFsj-000O6HC; Sun, 25 Oct 92 23:52 SAST Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA06936; Sun, 25 Oct 92 23:55:30+020 From: gavan@za.ac.uct.mth.elc (Gavan Tredoux) Message-Id: <9210252155.AA06936@elc.mth.uct.ac.za> Subject: Type checking loophole? To: info-hol@edu.uidaho.cs.ted (Info-hol mailing list) Date: Sun, 25 Oct 92 23:55:28 EET X-Mailer: ELM [version 2.3 PL11] I've defined a new type ":lnum" and a constant "holds" but some typos revealed the following phenomenon. Transcript follows from hol2.0 -------------------------------------------------------------- type_of "WHOLE";; ":num -> lnum" : type type_of "holds";; ":exseq -> (lnum -> (wff -> bool))" : type "!e i fmla. holds e(WHOLE i)((ALL fmla) imp fmla)";; "!e i fmla. holds e(WHOLE i)((ALL fmla) imp fmla)" : term "!e i fmla. holds e (i) ((ALL fmla) imp fmla)";; "!e i fmla. holds e i((ALL fmla) imp fmla)" : term -------------------------------------------------------------- This shouldn't be allowed, the second term with "holds" having an ":int" rather than an ":lnum" for the second argument. Yet the parser okays both. Hmm. Gavan Tredoux FACCS Lab UCT