[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]
makarius at sketis.net
Fri Apr 12 22:00:06 CEST 2013
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
> The following may or may not be related: I recently spent some thought
> on getting rid of the mandatory vs optional distinction of qualifiers.
> In any case this will likely have considerable impact, so here's the
> Currently there is the strange feature that abbreviations are only
> unfolded under morphisms that are the identity on term parameters.
Unfolding should always work, problems arise when folding back for printed
Here is an example:
locale foo =
fixes xxx :: nat
abbreviation "yyy == Suc xxx"
interpretation foo 0 .
term yyy -- "Suc 0"
Here the unfolding is done, the folding is not done.
Adding a prefix to the interpretation should merely change name space
accesses (IIRC, without looking at the factual situation in the sources).
> From what I see on the mailing lists this has confused users. Instead,
> I would propose to change the criterion to that abbreviations are only
> unfolded under morphisms that do not change the name part (i.e. without
> qualification). This would mean that for an unqualified instance syntax
> remained available while for a qualified instance syntax redeclaration
> would be necessary.
When you say "syntax", do you mean concrete syntax (notation), abstract
syntax (name accesses and abbreviations) or both?
I reckon that the tentative 'private' modifier would affect all that
> This would, of course, require some experimentation, but for now I just
> would like to learn whether the 'private' modifier would be related and
> should be taken into consideration.
I think it is somewhere in the same cloud of possibilties. Once it clears
up a little, we should see the necessary conclusions, and what is right.
More information about the isabelle-dev