[Developers] finite map EVAL question
Ramana.Kumar at cl.cam.ac.uk
Thu Oct 6 05:44:19 UTC 2016
(By the way, I think that question should really go to
hol-info at lists.sourceforge.net :).)
On 6 October 2016 at 16:43, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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