overloading/overriding of variables in basic specs

[Don Sannella <dts@dcs.ed.ac.uk>]

When relaxation of the restrictions in v0.95 on multiple uses of
identifiers in basic specs was discussed in Paris and Lille, I thought
the conclusion for variables was as follows:

   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.

At any rate, this is what I recorded in the final version of Note S-1
in the section on variable declarations [2.2], to discharge a question
there.

In v0.97 I can find no trace of the restriction in the second half of
the first sentence (that overriding of variable declarations as basic
items is forbidden).  But such a restriction is unavoidable given the
decision to forbid overloading of variables and the decision to take
non-linear visibility: if a variable can be declared with different
sorts then we have to say which declaration is the one that counts,
and if the order of declarations is irrelevant then there is no
reasonable basis on which to make this decision.

[Right, it seems that I overlooked the business of explaining about
overriding.  I guess we can simply add the wording above in v0.98, OK?
--PDM]

The problem doesn't arise with linear visibility, and it doesn't arise
for variable declarations within quantifications because nesting
imposes an order on declarations.

[Personally, I'd prefer to ban overriding altogether, for
methodological reasons: it can be quite confusing, when seeing a
variable in a term/axiom, to have several declarations for it in the
enclosing text - one may might overlook the relevant one.  But I hope
that tools will be able to warn us of such things, so I don't object
to allowing overriding (if it also makes the semanticists' job easier :-) 
--PDM]

(Peter, while I'm here, I noticed a couple of mis-spellings:
	section 2.1: cosntructor
	section 2.3.3: particlar)

[For some reason (?) i-spell stopped working when the staff here
installed a new version of it.  And I haven't had time enough for
proper careful proof-reading lately, sorry.  Thanks.  --PDM]

Regards, Don