Re: [Haskell-cafe] Stuck in proof of trivial compiler

On Wed, Sep 9, 2015 at 3:24 PM, Jonas Scholl 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?