Pattern matching against nat

[robsimmons]

The following code errors in code production when I try to produce a pattern match against the constructor "_plus" corresponding to the built-in interpretation of "A + B".

w: world.

term: string -> t -> rel @ w.       // T
nonterm: t -> t -> t -> rel @ w.    // NT
parse: t -> nat -> nat -> rel @ w.  // PROD
tok: nat -> string -> rel @ w.      // IN

// Generic rules of parsing

term S T, tok I S -> parse T I I.
nonterm X Y Z, parse Y I J, parse Z (J+1) K -> parse X I K.

[robsimmons]

This is like issue #8 but simpler, because here we already know what J is and so it shouldn't be an issue to add 1 to it.