[isabelle-dev] comparison of bindings
boehmes at in.tum.de
Sun Jun 26 14:23:41 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. Using
Binding.print to turn a binding into a string (and using Symtab.table)
doesn't seem to be the right approach (Binding.print is probably not
meant for this purpose). What should be used instead?
More information about the isabelle-dev