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 14:15:10 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22458; Tue, 12 Jan 93 05:58:42 -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 AA22453; Tue, 12 Jan 93 05:58:28 -0800 Received: by koudai.cs.titech.ac.jp (5.67+1.6W/koudai); Tue, 12 Jan 93 22:57:41 JST Received: by jevex.cs.titech.ac.jp (16.7/css1.5); Tue, 12 Jan 93 22:57:55 +0900 Message-Id: <9301121357.AA05118@jevex.cs.titech.ac.jp> To: info-hol@edu.uidaho.cs.ted Cc: kikuchi@jp.ac.titech.cs Subject: APPLY function on HOL In-Reply-To: Your message of "Sat, 09 Jan 1993 20:28:14 JST." <9301091128.AA09894@cake.cs.titech.ac.jp> Date: Tue, 12 Jan 1993 22:57:54 JST From: KIKUCHI Yutaka Hello, everyone. I have two questions about HOL. So won't you give me your company for my questions? 1. I want to define a function that takes two arguments, the first one is an arbitrary type function, the second one is an argument for the first. For example, we can use APPLY function in LISP for the perpose. (apply #'+ '(1 2 3)) => 6 In HOL, I guessed that the following would be okay, but It was a wrong guess. new_recursive_definition false list_Axiom `APPLY` "(APPLY f [] = f) /\ (APPLY f (CONS h tl) = APPLY (f h) tl)";; How can I define such a function? 2. "node [node [node []];node[]]";; causes an error as the following skipping: ] ; node [ ] ] " ;; parse failed in HOL ver.2.01, although it is acceptable in HOL ver.2.00. "node [node [];node [node []]]";; makes no error in the both versions. Is it a bug of HOL2.01 or something wrong with me? Thank you very much. -- KIKUCHI Yutaka, The Department of Computer Science, Tokyo Institute of Technology Ookayama, Meguro, Tokyo 152 Japan E-mail: kikuchi@cs.titech.ac.jp Tel: +81-3-3728-7663 Fax: +81-3-3728-5021