Talk:Exchange lemma

From The Twelf Project

[edit] Needs more information?

I understand what's going on in this article, and think it's a good thing to show, but I think the article needs a descripition of how this would be encountered in practice - how the explicit exchange metatheorem would actually be avoided by rearranging the order of the lambdas... — Rob (and his talk) 19:03, 27 September 2006 (MST)

I editted the commentary on the code snippet to point to the substitution lemma example where it is being used. I'm not sure if there's a better/simpler example that could just be inlined. --DanielKLee 19:45, 27 September 2006 (MST)

The code doesn't have to make LOTS of sense out of context - for me, it helps to just see it. What do you think of these changes? — Rob (and his talk) 20:28, 27 September 2006 (MST)

This snippet works for me. I re-worded it slightly and fixed a missing </tt>. --DanielKLee 20:43, 27 September 2006 (MST)