Talk:Using nat-less with %reduces

From The Twelf Project

What do you think about turning this into a tutorial on strong induction over natural numbers?  — Tom 7 11:45, 28 September 2006 (MST)

Makes sense to me, as it's an extention of the %reduces article. Also, some of the code may need to be jiggled to work correctly with the parser - I'll add it to the parser to do list, but I'm not sure I can get it to *not* highlight thing1 in:

name-of-metatheorem : {N}
    thing1 N z N
    -> thing2 z N N
    -> type.

— Rob (and his talk) 15:09, 28 September 2006 (MST)

That might be a good idea. Any fun ideas for a theorem to prove using strong induction? The other target for the "Strong induction" tutorial would be the nat-division stuff, which already has an example of using %reduces to get the induction right. --DanielKLee 15:55, 28 September 2006 (MST)