[isabelle-dev] comparison of bindings

[Alexander Krauss]

Hi,

> 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. 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.). I never did the latter, 
though.

Alex