[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.
Michael
More information about the Developers
mailing list