<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The proposed type of exported theorems above makes it clear that we<br>
need a way to merge metadata if two alpha-equivalent theorems are<br>
exported. It also shows that two different theorems may have identical<br>
metadata without causing confusion.<br></blockquote><div><br>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.<br><br></div><div>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.<br><br>Mario<br></div></div></div></div>