Florian Haftmann wrote:
What I have to address is that
you cannot be sure that a given name is already used, regardless how
many prefices you add.
There is a bit more to this story:
Ideally, the internals of a package should be completely invisible
unless a user explicitly chooses to look at them (eg. by looking at
concealed facts), which is always at your own risk... Traditionally,
packages made no real attempt at hiding their stuff, but the recent
Binding.conceal efforts try to move towards this.
What Florian tries to avoid with "liberal bindings" is the following
situation, which can be illustrated nicely using the function package:
definition "f_graph = True"
fun f where "f x = x"
*** Duplicate constant declaration "Scratch.f_graph" vs. "Scratch.f_graph"
But the symmetric situation would not be avoided by a liberal binding alone:
fun f where "f x = x"
definition "f_graph = True"
(here we get a type error instead, by mere coincidence)
It would be nice if we could find a convention that avoids both kinds of
errors. In principle, a combination "liberal + prefix" could do this...
On the other hand, if I add the prefix "function_package_INTERNAL"ΒΈ it
is unlikely that a clash will ever occur in practice. So I am not sure
if we really need a new concept...
Alex
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
