<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="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.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">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</blockquote></div><br></div>