Add numerals syntax for natural numbers
I believe allowing numerals to be used in the syntax would make the user-experience much more natural. For now however, making this addition could lead to the same issues that arose with universe polymorphism, being that the unary encoding could easily lead to stack-overflows. Would the kernel benefit from handling natural numbers in a special way, or would handling them during parsing/elaboration be enough for now ?