Talk:%reduces

From The Twelf Project

[edit] Splitting this up

At this point, this article is pretty incomplete as there is still much to be said about the %reduces directive. I did want to get a code example in, though. The addition of the nat-less-reduces stuff makes the code example longer than necessary. We might want to just cut it off after nat-plus-reduces-s or nat-plus-reduces and have the entire proof of nat-less-reduces as its own code example/tutorial. --DanielKLee 10:08, 27 September 2006 (MST)

• In my opinion it's important to be as brief as possible with code snippets; they should be only the minimal size needed to illustrate the relevant point. Perhaps breaking it up into two sections would be the right way to go.  — Tom 7 10:39, 27 September 2006 (MST)