<div dir="ltr">Dear Joe,<div><br></div><div>Looks like there is again a problem with the number of proofs we have:</div><div><div># List.length (list_the_exported_thms ());;</div><div>val it : int = 1231</div><div># List.length (search[]);;</div><div>val it : int = 1686</div></div><div><br></div><div>Could you please update them also?</div><div>Thanks a lot.</div><div>Robert</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 13 July 2015 at 23:44, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks a lot Joe,<div><br></div><div>I will merge it up :)</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Robert</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 13 July 2015 at 23:06, 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 Robert,<br>
<br>
If you pull the most recent version of the OpenTheory HOL Light fork,<br>
you can use<br>
<br>
list_the_exported_thms ();;<br>
<br>
to show a list of exported theorems together with the theory they were<br>
exported to (i.e., the argument to logfile).<br>
<br>
Hopefully that's the information you require.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
On Fri, Jul 10, 2015 at 12:55 AM, Robert White<br>
<div><div><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
> Thanks for the reply.<br>
><br>
> Yeah, such a function would be helpful<br>
><br>
> Regards<br>
> Robert<br>
><br>
> On Jul 9, 2015 8:35 PM, "Joe Leslie-Hurd" <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:<br>
>><br>
>> Hi Robert,<br>
>><br>
>> Whenever an article is generated, it is normalized so that if a type<br>
>> or term is used multiple times then it is built once, saved in a<br>
>> dictionary, and then pulled out when needed. For theorems this is<br>
>> taken even further, so that theorems that are alpha-equivalent are<br>
>> only constructed once.<br>
>><br>
>> I'm afraid there's currently no infrastructure for recording which<br>
>> article file a theorem was exported to in HOL Light. It probably<br>
>> wouldn't be too hard to add, though, if you needed the information.<br>
>><br>
>> Cheers,<br>
>><br>
>> Joe<br>
>><br>
>><br>
>> On Thu, Jul 9, 2015 at 5:12 AM, Robert White<br>
>> <<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
>> > Dear Joe,<br>
>> ><br>
>> > I wonder what's behind OpenTheory when it's merging two or more article<br>
>> > files together. Is there any optimization?<br>
>> ><br>
>> > By the way, for HOL Light, is there any function I can tell which thm is<br>
>> > in<br>
>> > which article file after exporting?<br>
>> ><br>
>> ><br>
>> > Thanks a lot!<br>
>> ><br>
>> > --<br>
>> ><br>
>> > Regards,<br>
>> > Robert White (Shuai Wang)<br>
>> > INRIA Deducteam<br>
>> > [Moving to ILLC of UvA from this Sep to continue my masters. ]<br>
>> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]<br>
>> ><br>
>> ><br>
>> > _______________________________________________<br>
>> > opentheory-users mailing list<br>
>> > <a href="mailto:opentheory-users@gilith.com" target="_blank">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>
>> ><br>
>><br>
>> _______________________________________________<br>
>> opentheory-users mailing list<br>
>> <a href="mailto:opentheory-users@gilith.com" target="_blank">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>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">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>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">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><br clear="all"><div><br></div>-- <br><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div>
</div>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div>
</div>