Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id UAA10559; Tue, 10 Oct 1995 20:27:31 +0200 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA229936239; Tue, 10 Oct 1995 08:43:59 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: list Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA229906238; Tue, 10 Oct 1995 08:43:58 -0600 Received: from tuminfo2.informatik.tu-muenchen.de (tuminfo2.informatik.tu-muenchen.de [131.159.0.81]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with ESMTP id HAA13065 for ; Tue, 10 Oct 1995 07:43:27 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26524-4>; Tue, 10 Oct 1995 15:43:10 +0100 Received: by sunbroy14.informatik.tu-muenchen.de id <8083>; Tue, 10 Oct 1995 15:42:55 +0100 From: Konrad Slind To: shaw@cs.ucdavis.edu, info-hol@cs.uidaho.edu In-Reply-To: <199510092354.QAA19306@roma-cafe.cs.ucdavis.edu> (shaw@cs.ucdavis.edu) Subject: Re: ACCEPT_TAC nit pick... Message-Id: <95Oct10.154255met.8083@sunbroy14.informatik.tu-muenchen.de> Date: Tue, 10 Oct 1995 15:42:41 +0100 Rob Shaw writes > - g `!m. ~(m < m)`; > ... > Initial goal proved. > |- !n. ~(n < n) : goalstack This is a place where theory meets practice. Lambda calculus theory (and HOL) treats alpha-equivalent terms as identical. However, users often want the names that they choose to be preserved. To implement this requires a finer notion of equality: "identical trees". OK, this can be implemented easily, for example by making terms into an "equality" type. However, in this case a "user-friendly" ACCEPT_TAC needs to execute two tests: one for tree identity and one for alpha-convertibility. Is the added complexity worth it? Konrad.