[isabelle-dev] NEWS: limited name space accesses
makarius at sketis.net
Thu Apr 9 16:42:41 CEST 2015
On Tue, 7 Apr 2015, Makarius wrote:
> 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 languages.
> 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 problems like
> qualified lemma a: ...
> lemma b (qualified c): ...
> lemma e (qualified f!): ...
After thinking about this again, it looks like the following is feasible:
private lemma a: ... -- "no name space accesses"
qualified lemma a: ... -- "only qualified name space accesses"
later, after the release:
lemma x.y.a: -- "qualified 'base' name leading to mandatory accesses"
This means Binding.qualified is not involved here at all. The second
reform merely allows Binding.name / Binding.make with already qualified
names. There will be further consequences from this that we can explore
after the release, such as Free variables with qualified names.
The 'private' / 'qualified' command above prefixes are technically already
there, and I will just make one more round of renaming before we get onto
the release lane.
More information about the isabelle-dev