[Haskell-cafe] Stuck in proof of trivial compiler

Rustom Mody rustompmody at gmail.com
Wed Sep 9 13:25:10 UTC 2015

On Wed, Sep 9, 2015 at 3:24 PM, Jonas Scholl <anselm.scholl at tu-harburg.de>

> How about trying to prove the following:
> mac (compile e ++ x) s = mac x (eval e : s)
> You can then just break down your term into pieces, build up the stack
> and evaluate it in your prove.

Thanks Jonas, Janis
I knew I had to generalize it but not in '2 dimensions' -- x and s !
Seems obvious on further reflection
I wonder though what is the moral for formulating theorems of right
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150909/82c97650/attachment.html>

More information about the Haskell-Cafe mailing list