[opentheory-users] Theorem meta-data

[Mario Carneiro]

> The proposed type of exported theorems above makes it clear that we
> need a way to merge metadata if two alpha-equivalent theorems are
> exported. It also shows that two different theorems may have identical
> metadata without causing confusion.
>

This made me realize a potential issue in the current spec and even the
version 5 spec: the theorem export list is described as a "set", even
though my own implementation just treats it as a list. What is supposed to
happen if you export two alpha-equivalent theorems? Do you keep them both,
or throw away the original one or the new one? With metadata, this becomes
still more complicated. My java implementation would have issues with using
a HashMap for the thm keys of that map, because I have no hash function
that respects alpha-equivalence. And if there are two alpha-equivalent
theorems being exported in the same file, then that means that article
readers too will have to handle metadata merging.

Incidentally, are you in agreement with using a name -> object finite_map
for the metadata? Using names seems the easiest way to build in namespaces
the way you were originally thinking, and works well with the rest of the
machine.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141109/6d251b24/attachment.html>