[Developers] finite map EVAL question
Ramana.Kumar at cl.cam.ac.uk
Thu Oct 6 05:43:02 UTC 2016
We mostly don't use the default EVAL compset, but instead build things up
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.
> Developers mailing list
> Developers at cakeml.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers