Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 26 Oct 1992 15:06:46 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28556; Mon, 26 Oct 92 06:54:38 -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 AA28551; Mon, 26 Oct 92 06:54:32 -0800 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA09516; Mon, 26 Oct 92 09:53:20 -0500 Message-Id: <9210261453.AA09516@air52.larc.nasa.gov> Date: Mon, 26 Oct 92 09:53:20 -0500 From: Victor "A." Carreno To: gavan@za.ac.uct.mth.elc Subject: Re: Type checking loophole? In-Reply-To: Mail from 'gavan@elc.mth.uct.ac.za (Gavan Tredoux)' dated: Sun, 25 Oct 92 23:55:28 EET Cc: info-hol@edu.uidaho.cs.ted gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes: > 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. In the first instance the term "i" has type ":num". In the second instance the term "i" indeed has a type ":lnum". Try the following: "!e i fmla. holds e (i) ((ALL fmla) imp fmla)";; "!e i fmla. holds e i(ALL fmla imp fmla)" : term "!e (i:num) fmla. holds e (i) ((ALL fmla) imp fmla)";; Badly typed application of: "holds e" which has type: ":lnum -> (wff -> bool)" to the argument term: "i" which has type: ":num" evaluation failed mk_comb in quotation Victor.