Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Tue, 12 Jan 1993 18:46:43 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22996; Tue, 12 Jan 93 10:32:23 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from koudai.cs.titech.ac.jp by ted.cs.uidaho.edu (16.6/1.34) id AA22991; Tue, 12 Jan 93 10:32:14 -0800 Received: by koudai.cs.titech.ac.jp (5.67+1.6W/koudai); Wed, 13 Jan 93 03:31:26 JST Received: by jevex.cs.titech.ac.jp (16.7/css1.5); Wed, 13 Jan 93 03:31:40 +0900 Message-Id: <9301121831.AA05590@jevex.cs.titech.ac.jp> To: David Shepherd Cc: kikuchi@jp.ac.titech.cs (KIKUCHI Yutaka), info-hol@edu.uidaho.cs.ted Subject: Re: APPLY function on HOL In-Reply-To: Your message of "Tue, 12 Jan 1993 14:30:49 GMT." <1818.9301121430@frogland.inmos.co.uk> Date: Wed, 13 Jan 1993 03:31:40 JST From: KIKUCHI Yutaka 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 -- Yu.