Comment by LessDmesg

What always puzzled me is why any of these dependent type people continue using unary numbers, even at the type level. Unary numbers are a surefire way to show that a programming language is utterly impractical and its authors are noobs. Is it really that hard to embed decimal numbers with integral arithmetic to the type level instead of permanently Succ'ing the Coq?