[CakeML-Dev] CF to translator
Ramana.Kumar at cl.cam.ac.uk
Sat Oct 8 11:24:28 UTC 2016
> I'm happy to make a minor tweak to the definition of st2heap and prove
> the following. I would appreciate help with proving lemma 2 from the
No problem. I've replaced my cheated lemma 2 by the one you said you'd
provide (i.e. I proved what I need from that).
On 7 October 2016 at 22:06, Armaël Guéneau <armael.gueneau at ens-lyon.fr>
> On 07/10/2016 12:39, Magnus Myreen wrote:
>> I have proved the following connection between CF's app_basic (as on
>>> master) and a revised formulation of the translator's Arrow, modulo 4
>>> cheats. In this email, I will show: the final theorem proved, the cheated
>>> lemmas, and the new Arrow definition. I ask for the following feedback:
>>> 1. Does the final theorem look like a strong enough connection?
>> Probably yes. I think Armaël might know better than me.
> Yes, I think it's strong enough.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers