On Sun, 26 Jun 2011, Alexander Krauss wrote:
Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?
Here is a more concrete example. Assume there is a declaration such
as:
declare_foo name = ...
which declares "name" as some new foo-entity. For later reference,
the declared foo-entities are best stored in a table internally,
associated with the declaration data (the omitted right-hand side
above). Indexing this table with the binding produced from "name" is
not possible, as bindings cannot be compared with each other.
As I understand it, it is not the purpose of a binding to identify an object
during its whole lifetime, but only as a recipe for producing a namespace
entry (possibly after applying some modifications via morphisms etc.).
So I would expect that at some point you actually produce an actual name
before you store the foo in the table.
Yes, exactly.
Depending on the application, you could either just use the base name or
qualified name (Binding.(qualified_)name_of) or use a full-blown
namespace (with optional qualifiers, concealed entries etc.).
Binding.qualified_name_of is not the right thing, and in fact I have
discontinued it a few days ago, because it was unused (and confusing).
In the life-cycle of name bindings, you always converge towords long names
and name space entries. See also Name_Space.full_name,
Name_Space.declare, Names_Space.define etc.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
