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
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html
qualified lemma a: ...
lemma b (qualified c): ...
lemma e (qualified f!): ...
After thinking about this again, it looks like the following is feasible:
now:
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
