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; Thu, 27 Jan 1994 21:02:27 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17235; Thu, 27 Jan 1994 13:47:35 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from uafhp.uark.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA17229; Thu, 27 Jan 1994 13:47:33 -0700 Received: from csci0.uark.edu by uafhp.uark.edu with SMTP (1.37.109.4/15.6) id AA27914; Thu, 27 Jan 94 14:42:10 -0600 Received: by domain_csci (4.1/SMI-4.1) id AA26416; Thu, 27 Jan 94 14:38:41 CST Date: Thu, 27 Jan 1994 14:38:40 -0600 (CST) From: Sam Nelson Subject: HOL Qs To: info-hol@leopard.cs.byu.edu Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII I've been trying to work with hol for some time, but I've been having trouble making much progress. It seems that when I run into a snag that I lack the expertese to know how to get unsnagged. I hope that this is an appropriate forum for getting help with hol, even if some of my problems may be fairly simple ones. Currently I`m trying to reduce ". |- n < m". down to a boolean value. However, when I try to use a REWRITE_RULE for LESS, hol spits it out. Does this occur because LESS is an infix definition? Can anybody tell me what I need to do? Sam Nelson snelson@csci0.uark.edu