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