Hi Florian,
you are right, I was thinking more from a user perspective, whereas your
point is on the package developer side. Sorry, for my misinterpretation.
What I meant is that as a user, you can be sure that names that are
automatically generated by packages (assuming that they use binding
prefixes and respect each others naming conventions) are different from
whatever name you could invent. (Is that true? Excluding Isabelle/ML.)
Only as a package developer, you have to make sure that whatever names
you invent, are not used by other packages. For this purpose, I think
your "liberal" flag makes perfect sense. As long as the user does not
have to care about it at all.
Assuming I give some inductive definition:
inductive foo :: "..." where
"..." |
"..."
Then, as a user, I count on the name "foo.intros" and it would not be
nice to get some variant, just because "inductive" marked its generated
names as "liberal". I think, what I'm trying to say, is that package
authors should be careful in cases where they produce names that are
visible to the user. But that's a truism anyway ;)
cheers
chris
On 10/08/2010 09:18 AM, Florian Haftmann wrote:
Hi Christian,
to me the liberal flag seems rather ad-hoc. Wouldn't a proper
hierarchical naming solve this problem (maybe by introducing an
automatic "sub-module" Internal/Auto/Whatever for any theory T, such
that automatic names may be referred to by using
T.Whatever.automatic_name).
we *have* already the concept of binding prefices (what you refer to
here as hierarchical naming), although the theory name part of the
prefix currently is always a singleton. What I have to address is that
you cannot be sure that a given name is already used, regardless how
many prefices you add.
Cheers,
Florian
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
