[Developers] finite map EVAL question

[Ramana Kumar]

We mostly don't use the default EVAL compset, but instead build things up
manually.
However, that probably means using finite_mapLib's compset, which would
presumable get this addition.
I think those theorems seem reasonable to add...

On 6 October 2016 at 14:58, <Michael.Norrish at data61.csiro.au> wrote:

> Testing the new list:
>
> Would it be unreasonable to add o_f_FEMPTY
>
>   |- f o_f FEMPTY = FEMPTY
>
> and o_f_FUPDATE
>
>   |- f o_f (fm |+ (k,v)) = (f o_f (fm \\ k)) |+ (k, f v)
>
> to the standard EVAL compset in HOL?  (Note that the \\ is unnecessary in
> this theorem; perhaps it should be removed.)
>
> I reckon CakeML folk are probably among the heaviest users of EVAL, and so
> might have pertinent opinions.
>
> Michael
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161006/88678f22/attachment.html>