[Developers] finite map EVAL question

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Thu Oct 6 03:58:36 UTC 2016

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. 


More information about the Developers mailing list