[isabelle-dev] comparison of bindings

[Makarius]

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