<div dir="ltr"><div><div>I like your original theorem metadata proposal better.<br><br></div>But I suppose one could follow your approach with an extra article that adds names, if one needs names right now.<br><br></div><div>It may be right to wait for more field testing, that's up to you. Certainly if I actually end up hacking up custom encoding/decoding schemes for metadata, I'll keep the list informed.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 27 October 2015 at 15:28, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<span class=""><br>
> It looks like you are encoding theorem names via some (undocumented) scheme<br>
> that wraps the theorem as:<br>
><br>
>   |- (\name_of_thm. name_of_thm) conclusion_of_thm<br>
><br>
> Is this going to become a standard format in which to encode theorem names,<br>
> that other article readers should expect? (I presume not!)<br>
<br>
</span>It didn't take you long to reverse engineer my little hack to annotate<br>
theorems with names! Have no fear, my intention is that this scheme is<br>
private to the HOL Light/OpenTheory interface, which is why the scheme<br>
is undocumented, and the corresponding metadata files in the theory<br>
package suggest that they are to be used by HOL Light only:<br>
<br>
<a href="http://hol-light.int" rel="noreferrer" target="_blank">hol-light.int</a>  --  Mapping the OpenTheory namespace to HOL Light names<br>
hol-light.art  --  Mapping the set of theorems to HOL Light names<br>
<br>
This fits with the existing scheme whereby some theories can be<br>
exported as Haskell packages, and there are haskell* metadata files in<br>
the theory package to help perform this export. Naturally other<br>
theorem provers are welcome to use the HOL Light files in their own<br>
interface, or alternatively could contribute metadata files of their<br>
own to the theory package.<br>
<span class=""><br>
> When we last discussed theorem names,<br>
> (<a href="http://www.gilith.com/opentheory/mailing-list/2014-November/000438.html" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list/2014-November/000438.html</a><br>
> and the ensuing discussion), the plan was to standardise on theorem<br>
> metadata. Has there been any progress on this front?<br>
<br>
</span>Thank you for exhuming the theorem metadata proposal from the archive.<br>
Even a year later I still like the idea of changing the type of<br>
exported theorems from<br>
<br>
thm set<br>
<br>
to<br>
<br>
(thm, metadata) finite_map<br>
<br>
using a scheme for merging meta-data such as the one I sketched out.<br>
However, perhaps it is better to see how the current scheme with extra<br>
metadata files evolves before committing to a standard metadata<br>
scheme?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div>