<div dir="ltr">Dear Joe,<div><br></div><div>Thanks very much for the reply. </div><div><br></div><div>It looks interesting that we can also play with it in Haskell but I'm not good at Haskell yet.</div><div><br></div><div>Thanks again!</div><div>Regards</div><div>Robert</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 19 May 2015 at 19:09, 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>
This is something I've been working on recently - it means that there<br>
are definitions in the theory package that can be exported as a<br>
Haskell package. For example, the definitions in base are exported to<br>
the "opentheory" package on Hackage:<br>
<br>
<a href="http://hackage.haskell.org/package/opentheory" target="_blank">http://hackage.haskell.org/package/opentheory</a><br>
<br>
In general, the Haskell package name is simply the theory name with<br>
"opentheory-" prepended, unless there is an explicit haskell-name<br>
declaration in the theory file that overrides this.<br>
<br>
You can find some (mostly outdated) information on a previous version<br>
of this Haskell export in the "Maintaining Verified Software" paper<br>
and talk at the bottom of<br>
<br>
<a href="http://www.gilith.com/research/opentheory/" target="_blank">http://www.gilith.com/research/opentheory/</a><br>
<br>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
On Tue, May 19, 2015 at 5:54 AM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear OpenTheory users and developers,<br>
><br>
> Hello.<br>
> I wonder if there is any reason there is a "Haskell" part in the base?  And<br>
> what does that mean exactly?<br>
><br>
> Thanks!<br>
><br>
> --<br>
><br>
> Regards,<br>
> Robert White (Shuai Wang)<br>
> INRIA Deducteam<br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><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></div></div></div></div></div></div></div>
</div>