<div dir="ltr"><div><div> OK. From the previous discussion it seems that cakeML provides <br>implementations for equality, when it can. My question arose in a <br>situation where I am working in HOL and using the HOL->cakeML<br>
translator. This brings me to a related question: since logical equality<br></div>is much more powerful than computational equality could it be that<br>a program is proved correct but that the generated equality code<br></div>
<div>isn't enough to enforce the property?<br><br></div><div>Konrad.<br><br></div><div><div><div><br>   <br><div><div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, May 20, 2014 at 6:53 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</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">(This kind of question could go on the non-private currently very-quiet <a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a> list :))<br>
</div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div class="h5">On Mon, May 19, 2014 at 11:27 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br>


</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">Very good!   --Konrad.<br><br></div><div><div><div class="gmail_extra">
<br><br>

<div class="gmail_quote">On Mon, May 19, 2014 at 5:11 PM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This should be fine. The underlying CakeML polymorphic equality will be used, which can be problematic for some types (e.g., those that can contain functions, or that represent sets as various non-canonical tree structures), but should be fine for the regexp type (now that char sets are bitvectors).<br>




<span><font color="#888888"><br>
-Scott<br>
</font></span><div><div><br>
On 2014/05/19, at 22:54, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
<br>
> Hi all,<br>
><br>
>   In the regexp compiler I have a test to see whether something<br>
> on the worklist has already been seen. This has the form<br>
><br>
>    if MEM r seen then ... else ...<br>
><br>
> How do the translator and cakeML handle MEM? Should I instead write<br>
> a version of MEM parameterized by a regexp equality predicate?<br>
><br>
> Thanks,<br>
> Konrad.<br>
><br>
<br>
</div></div></blockquote></div><br></div>
</div></div><br></div></div>_______________________________________________<br>
Dev mailing list<br>
<a href="mailto:Dev@cakeml.org" target="_blank">Dev@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/dev" target="_blank">https://lists.cakeml.org/listinfo/dev</a><br>
<br></blockquote></div><br></div>
<br>_______________________________________________<br>
Dev mailing list<br>
<a href="mailto:Dev@cakeml.org">Dev@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/dev" target="_blank">https://lists.cakeml.org/listinfo/dev</a><br>
<br></blockquote></div><br></div></div></div></div></div></div></div></div></div>