Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <17696-0@swan.cl.cam.ac.uk>; Sun, 9 Aug 1992 18:11:45 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA24779; Sun, 9 Aug 92 09:55:12 -0700 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 AA24774; Sun, 9 Aug 92 09:55:06 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <17530-0@swan.cl.cam.ac.uk>; Sun, 9 Aug 1992 17:53:22 +0100 To: toal@edu.ucla.cs (Ray J. Toal) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: need more pattern support? In-Reply-To: Your message of Thu, 06 Aug 92 12:20:18 -0700. <9208061920.AA29299@ewa.cs.ucla.edu> Date: Sun, 09 Aug 92 17:53:17 +0100 From: John Harrison Message-Id: <"swan.cl.ca.532:09.07.92.16.53.24"@cl.cam.ac.uk> Ray Toal suggests: > another useful contribution would allow HOL "functions" to look more like > functions in Standard ML. To a large extent you can make the HOL terms (including those in function definitions) look more like a functional language; for example there is a "LET" constant with built-in parser and prettyprinter support. You could add your own features through the parser and prettyprinter libraries. I imagine you are mainly thinking of more elaborate forms of recursive function definition (e.g. defining Quicksort). You can, I suppose, use an arbitrary recursion equation "let f x = t[f,x]" by just defining: f = @fn. !x. fn x = t[fn,x] but then to use the definition in any substantive way you have to show that: |- ?fn. !x. fn x = t[fn,x] Several people are working on ways of organizing the definition and proof together in a convenient way, maybe including automating certain kinds of recursion other than primitive. I don't know what progress has been made. John. P.S. Call me a pedant put I would have said: * another useful contribution would allow HOL functions to look more like * "functions" in Standard ML.