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, 30 Dec 1993 22:21:33 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01558; Thu, 30 Dec 1993 15:05:28 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.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 AA01554; Thu, 30 Dec 1993 15:05:14 -0700 Received: from inet-gw-2.pa.dec.com by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA01651; Thu, 30 Dec 1993 14:02:37 -0800 Received: by inet-gw-2.pa.dec.com; id AA12546; Thu, 30 Dec 93 09:18:28 -0800 Received: by evsrv3.afl.hlo.dec.com (5.57/ULTRIX-fma-041391); id AA10955; Thu, 30 Dec 93 12:18:08 -0500 Date: Thu, 30 Dec 93 12:18:08 -0500 From: leonard@evsrv3.afl.hlo.dec.com (Tim Leonard) Message-Id: <9312301718.AA10955@evsrv3.afl.hlo.dec.com> To: info-hol@cs.uidaho.edu Subject: What's TERM_MATCH in hol88? What's TERM_MATCH? It appears in a failure string that hol88 gave me, but it isn't described in the manual, and I didn't find anything by searching with grep "TERM_MATCH" hol/help/ENTRIES/* grep "TERM_MATCH" hol/ml/*.ml grep "TERM_MATCH" hol/lisp/*.l Is it simply a misleading message returned by match? Tim #let MATCH_EQ_CONV = PART_MATCH (fst o dest_eq);; #MATCH_EQ_CONV = - : (thm -> conv) #MATCH_EQ_CONV thm tm;; evaluation failed TERM_MATCH ... #match it tm;; evaluation failed TERM_MATCH #help `TERM_MATCH`;; evaluation failed help -- No information available on TERM_MATCH #TERM_MATCH;; unbound or non-assignable variable TERM_MATCH 1 error in typing typecheck failed