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 09:52:26 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25574; Wed, 13 Jan 93 01:38:14 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA25569; Wed, 13 Jan 93 01:38:05 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Wed, 13 Jan 1993 09:36:25 +0000 To: KIKUCHI Yutaka Cc: info-hol@edu.uidaho.cs.ted Subject: Re: APPLY function on HOL In-Reply-To: Your message of Wed, 13 Jan 93 03:31:40 +0200. <9301121831.AA05590@jevex.cs.titech.ac.jp> Date: Wed, 13 Jan 93 09:36:17 +0000 From: Richard Boulton Message-Id: <"swan.cl.ca.180:13.01.93.09.36.28"@cl.cam.ac.uk> > 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 The type of f needs changing to :**->*->**, i.e.: #new_recursive_definition false list_Axiom `ACCUM` # "(ACCUM (f:**->*->**) a [] = a) /\ # (ACCUM f a (CONS x xs) = ACCUM f (f a x) xs)";; |- (!f a. ACCUM f a[] = a) /\ (!f a x xs. ACCUM f a(CONS x xs) = ACCUM f(f a x)xs) Or the order of the arguments to f can be changed, i.e. (f a x) ---> (f x a): #new_recursive_definition false list_Axiom `ACCUM` # "(ACCUM (f:*->**->**) a [] = a) /\ # (ACCUM f a (CONS x xs) = ACCUM f (f x a) xs)";; |- (!f a. ACCUM f a[] = a) /\ (!f a x xs. ACCUM f a(CONS x xs) = ACCUM f(f x a)xs) Richard.