Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 2 Sep 1994 17:40:55 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02077; Fri, 2 Sep 1994 10:30:19 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA02071; Fri, 2 Sep 1994 10:30:14 -0600 Received: from relay.cs.ruu.nl (infix.cs.ruu.nl [131.211.80.7]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id JAA07628 for ; Fri, 2 Sep 1994 09:24:56 -0700 Received: from muddy.cs.ruu.nl by relay.cs.ruu.nl with SMTP id AA05651 (5.67a/IDA-1.5 for ); Fri, 2 Sep 1994 12:15:44 +0200 From: Wishnu Prasetya Received: (wishnu@localhost) by muddy.cs.ruu.nl (8.6.9/8.6.9) id MAA18343 for info-hol@ted.cs.uidaho.edu; Fri, 2 Sep 1994 12:15:43 +0200 Message-Id: <199409021015.MAA18343@muddy.cs.ruu.nl> Subject: treating infix To: info-hol@cs.uidaho.edu (hol mailing list) Date: Fri, 2 Sep 1994 12:15:42 +0200 (METDST) X-Mailer: ELM [version 2.4 PL23] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 666 I wonder if it may not be nicer to drop the special status of infix operators at the HOL level (ie it has to be declared with define_infix_etc). Why not introduce (more?) special symbols at the parsing level and arrange things such that any function OP: *A->*B->*C when written: "a $$OP b" will be parsed as "OP a b". We can even extend this mechanism to expression like: "$3IF (a