[isabelle-dev] comparison of bindings

Makarius 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
>> 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.


More information about the isabelle-dev mailing list