[CakeML-Dev] CF to translator

[Armaël Guéneau]

On 07/10/2016 12:39, Magnus Myreen wrote:
> Excellent!
>
>> 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.