[Haskell-cafe] Stuck in proof of trivial compiler
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...
More information about the Haskell-Cafe