> It would be, but the compiler recognizes the pattern and does ordinary integer arithmetic where it needs to (the pattern is relevant, however, to the use of individual natural numbers in defining other types, which is pretty important to Idris.)

The compiler does recognise it, because it'd be silly not to, but more importantly, Nats tend to be type level things which explain the structure of something else (e.g. a successor corresponds to a cons, or to another level in a tree), and as such don't appear in runtime code anyway. If what you want is machine arithmetic, better to use a type that's designed for that.

Idris has Haskell-like syntax because I like Haskell style syntax (this is probably the most important reason!) and Haskell programmers are the initial target audience.