[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

I guess, I should have specified that you're theory of expressions 
should support a notion of "alpha-equality" and capture avoiding 
substitution. I think, your Coq solution fails in that case.

Adam Chlipala wrote:
> {stuff deleted}
> I've used the most obvious encoding of variable binding.  The problem 
> almost seems "unfair" because a solution needn't prove any "semantic" 
> theorems, so the choice of binding mechanisms probably has little 
> (positive!) effect on how easy it is to complete the challenge.  At any 
> rate, this can serve at least as a baseline solution.  It's not long, 
> I've tried to comment it so as to be understandable to non-Coq experts, 
> and the link above includes a pretty-printed HTML version with comments 
> (via coqdoc).
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>