[Haskell-cafe] Stuck in proof of trivial compiler

[Rustom Mody]

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

> 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
generality?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150909/82c97650/attachment.html>