[isabelle-dev] comparison of bindings
krauss at in.tum.de
Sun Jun 26 21:08:25 CEST 2011
> 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
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,
More information about the isabelle-dev