[isabelle-dev] NEWS: limited name space accesses
makarius at sketis.net
Tue Apr 7 16:28:04 CEST 2015
On Tue, 7 Apr 2015, Tobias Nipkow wrote:
> On 07/04/2015 14:37, Christian Sternagel wrote:
>> (b) qualified
> That gets my vote because it expresses clearly the description Makarius
> gave: "name space entry that is only accessible by qualified names"
It is definitely good to collect keyword candidates from other well-known
I had "qualified" on my list of possibilities at first, but was hesitating
to use it, because there is yet another concept (c) that has no Isar
notation so far. It is called Binding.qualified in ML and could solve
lemma foo (qualified bar!): ...
In principle there could be a dual-use of 'qualified' as Binding.qualified
(with argument) and Name_Space.restricted (without argument), or rather
Name_Space.qualified after another "tuned signature" change.
qualified lemma a: ...
lemma b (qualified c): ...
lemma e (qualified f!): ...
This does not work in outer syntax though, since the new command prefix
category (keywords that may occur before a command) needs to be disjoint
from other minor keywords in the command body. (After the dismissal of
Proof General, command spans have become a bit more flexible, but cannot
be stretched arbitrarily.)
One could try to invent another notation for "x (qualified y!)" above.
Note that the "!" is the mandatory flag (like in locale interpretation
syntax). We don't have notation for such flags within qualified names
themselves. Otherwise one could use "c.b" directly.
A real danger in the whole affair is that we need to proceed towards the
Isabelle2015 release very soon, i.e. this week.
As a summary, here is the collection of nice keywords so far, without any
assignment of meanings yet:
More information about the isabelle-dev