Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 29 Sep 1992 17:33:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07413; Tue, 29 Sep 92 09:05:27 -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 AA07408; Tue, 29 Sep 92 09:03:41 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Tue, 29 Sep 1992 16:43:12 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Tom.Melham@uk.ac.cam.cl Subject: Re: Inheritance of binder status In-Reply-To: Your message of Tue, 29 Sep 92 14:41:49 +0700. <199209291341.AA15715@infix.cs.ruu.nl> Date: Tue, 29 Sep 92 16:42:57 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.650:29.08.92.15.49.31"@cl.cam.ac.uk> > I have defined ?? with new_binder_definition in theory, say, X. Then I > made theory Y, and declaring that X is a parent of Y. While the > definition of ?? is clearly now visible in Y, it seems that the binder > status is not inherited to Y. The question is, is this to be expected? > Is there any special reason for this, because it seems more natural to > me that such status be inherited to decendant theories, otherwise one > will be obliged to always insert new_binder `XX` for each binder XX > everywhere. Is there any special flag you can turn to do the trick? This is a long-standing bug, having something to do (I *think*) with the way in which the function parse_as_binder is defined using dml. Until it's fixed, you can always use "activate_all_binders". See the attached REFERENCE manual entry. Note that the COMMENT is (strictly speaking) false, but will become true once the bug is fixed. Tom ============================================================================= activate_all_binders : (string -> string list) SYNOPSIS Makes the quotation parser treat all binders in ancestor theories as such. DESCRIPTION The call activate_all_binders `thy` where thy is an ancestor theory (`-` stands for the current theory), will return a list of all binders on that theory and its ancestors, and make the parser treat them all as binders, that is, for each binder b, will allow the syntactic sugaring "b x. y" as a shorthand for "b (\x. y)". The special syntactic status may be suppressed by preceding b with a dollar sign. The function returns a list of all the binders dealt with. FAILURE CONDITIONS Never fails. COMMENTS This function is mainly intended for internal use. All binders declared by new_binder or new_binder_definition are always parsed as such anyway. SEE ALSO activate_binders binders new_binder parse_as_binder