Return-Path: <john.harrison-request@uk.ac.cam.cl>
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 19:31:11 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23215;
          Tue, 12 Jan 93 11:17:41 -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 AA23210; Tue, 12 Jan 93 11:17:32 -0800
Received: by koudai.cs.titech.ac.jp (5.67+1.6W/koudai);
          Wed, 13 Jan 93 04:16:47 JST
Received: by jevex.cs.titech.ac.jp (16.7/css1.5); Wed, 13 Jan 93 04:17:01 +0900
Message-Id: <9301121917.AA05632@jevex.cs.titech.ac.jp>
To: John Harrison <John.Harrison@uk.ac.cam.cl>
Cc: KIKUCHI Yutaka <kikuchi@jp.ac.titech.cs>, info-hol@edu.uidaho.cs.ted
Subject: Re: APPLY function on HOL
In-Reply-To: Your message of "Tue, 12 Jan 1993 14:39:09 GMT." <"swan.cl.ca.767:12.01.93.14.39.45"@cl.cam.ac.uk>
Date: Wed, 13 Jan 1993 04:17:00 JST
From: KIKUCHI Yutaka <kikuchi@jp.ac.titech.cs>

Dr. John Harrison said:
> The type system of HOL won't let you define such functions with quite
> the abandon of LISP.

I was so disappointed to hear that.
Our aim is to make a function that can apply [1;2;3] to +
and also can apply [2;3;4] to `\x y z.x+y*z'.
You mean that we cannot write such `apply' function, don't you?

-- Yu.