Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 13 Jan 1993 10:22:08 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25593; Wed, 13 Jan 93 02:09:52 -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 AA25588; Wed, 13 Jan 93 02:09:42 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Wed, 13 Jan 93 10:09:13 GMT From: David Shepherd Message-Id: <2942.9301131009@frogland.inmos.co.uk> Subject: Re: APPLY function on HOL To: kikuchi@jp.ac.titech.cs (KIKUCHI Yutaka) Date: Wed, 13 Jan 1993 10:09:39 +0000 (GMT) Cc: des@uk.co.inmos, kikuchi@jp.ac.titech.cs, info-hol@edu.uidaho.cs.ted In-Reply-To: <9301121831.AA05590@jevex.cs.titech.ac.jp> from "KIKUCHI Yutaka" at Jan 13, 93 03:31:40 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1100 KIKUCHI Yutaka has said: > Dr. David Shepherd said: > > first define an accumulate function (similar to ML's itlist) > > > > new_recursive_definition false list_Axiom `ACCUM` > > "(ACCUM (f:*->**->**) a [] = a) /\ > > (ACCUM f a (CONS x xs) = ACCUM f (f a x) xs)";; > > The definition causes an error as the following. > It seems that the error is the same as by our definition. > > #new_recursive_definition false list_Axiom `ACCUM` > "(ACCUM (f:*->**->**) a [] = a) /\ > (ACCUM f a (CONS x xs) = ACCUM f (f a ##x) xs)";; > Badly typed application of: "ACCUM f" > which has type: ":* -> ((**)list -> *)" > to the argument term: "f a x" > which has type: ":**" > > evaluation failed mk_comb in quotation silly error: it should be (f:**->*->**) -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq New Year Resolution for 1993: Start using capital letters.