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:44:17 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28615; Mon, 26 Oct 92 07:29:40 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28607; Mon, 26 Oct 92 07:29:18 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Mon, 26 Oct 92 15:13:59 GMT From: David Shepherd Message-Id: <11617.9210261513@frogland.inmos.co.uk> Subject: Re: Type checking loophole? To: des@uk.co.inmos (David Shepherd) Date: Mon, 26 Oct 1992 15:13:49 +0000 (GMT) Cc: gavan@za.ac.uct.mth.elc, info-hol@edu.uidaho.cs.ted In-Reply-To: <11551.9210261417@frogland.inmos.co.uk> from "David Shepherd" at Oct 26, 92 02:17:22 pm X-Mailer: ELM [version 2.4 PL3] Content-Type: text Content-Length: 649 David Shepherd has said: > Gavan Tredoux has said: > what would have been erroneous would be > > "! e (i:lnum) fmla. holds e (i) ((ALL fmla) imp fmla)";; ^ > and the type checker would have complained there is a deliberate mistake in the HOL term above ... i meant > "! e (i:num) fmla. holds e (i) ((ALL fmla) imp fmla)";; of course! -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq 1992: celebrate the quincentenary of columbus getting lost