[Developers] finite map EVAL question

[Ramana Kumar]

(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
> 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/b63874bd/attachment.html>