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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
