<div dir="ltr">(By the way, I think that question should really go to <a href="mailto:hol-info@lists.sourceforge.net">hol-info@lists.sourceforge.net</a> :).)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 6 October 2016 at 16:43, 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"><div><div>We mostly don't use the default EVAL compset, but instead build things up manually.<br></div>However, that probably means using finite_mapLib's compset, which would presumable get this addition.<br></div>I think those theorems seem reasonable to add...<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 6 October 2016 at 14:58,  <span dir="ltr"><<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.<wbr>au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Testing the new list:<br>
<br>
Would it be unreasonable to add o_f_FEMPTY<br>
<br>
  |- f o_f FEMPTY = FEMPTY<br>
<br>
and o_f_FUPDATE<br>
<br>
  |- f o_f (fm |+ (k,v)) = (f o_f (fm \\ k)) |+ (k, f v)<br>
<br>
to the standard EVAL compset in HOL?  (Note that the \\ is unnecessary in this theorem; perhaps it should be removed.)<br>
<br>
I reckon CakeML folk are probably among the heaviest users of EVAL, and so might have pertinent opinions.<br>
<br>
Michael<br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>