Syntactic sugar for natural numbers

[ccshan]

@davidweichiang says "Maybe we should add numbers to PERPL. Whenever I demo it, that is always what people balk at."

Something like Agda's BUILTIN NATURAL would be a great start.

Maybe @ariagivens wants to take this on...

[davidweichiang]

Cf. #47

[davidweichiang]

Yeah I think all that is really needed is

• [ ] predefined Nat, Zero, Succ
• [ ] number literals that desugar to Peano numbers

I think I’m okay with making programmers pattern match on Zero and Succ.

Then maybe:

• [ ] predefined plus and syntactic sugar for +
• [ ] predefined weigh