[isabelle-dev] comparison of bindings
makarius at sketis.net
Mon Jun 27 11:16:17 CEST 2011
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
>> 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.
> 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.
More information about the isabelle-dev