A variable declaration VAR-DECL determines sorted variables for use in axioms; it does not contribute to the signature. Such a declaration of a variable as a BASIC-ITEM abbreviates adding a universal quantification on that variable to all axiomsVAR-DECL ::= var-decl VAR+ SORT VAR ::= SIMPLE-ID
[HB,DTS,AT] That is, all later axioms
Discharged: No, because of non-linear visibility.in the enclosing BASIC-SPEC. The variables in the list VAR+ must be distinct,
[DTS] Presumably the items in the earlier lists SORT+, FUN-NAME+, PRED-NAME+ also have to be distinct?
Discharged: These variables no longer have to be distinct (neither do the items in the earlier lists) because multiple declarations are allowed.and distinct from the variables previously declared by other VAR-DECLs in the same list of basic items
[DTS] Is this also required when the VAR-DECL appears within a QUANTIFICATION? There is a comment later about overriding quantified variables which makes it seem not. What is the restriction, and is it the same for VAR-DECL as a BASIC-ITEM and VAR-DECL within QUANTIFICATION?
Discharged: Overriding a variable declaration is permitted for a VAR-DECL within a QUANTIFICATION, but not for a VAR-DECL as a BASIC-ITEM. But in the latter case a redeclaration of the same variable with the same sort is permitted, since multiple declarations are allowed.A simple identifier SIMPLE-ID for a variable may not be used simultaneously as the identifier of a sort, function, or predicate.
[DTS] Does this restriction apply also to variables in quantifications? (I guess so, but I'm not sure why the restriction is imposed)
Discharged: The restriction is eliminated.
[HB] Should variable declarations be put into the local environment, maybe in a separate mapping for variable names? ([DTS] These are part of the local environment, but their scope is just the rest of the current BASIC-SPEC.)
Discharged: No change required.