edwinb/Idris-dev — pull request #277 by andy-morris (2013-04-11 20:08:19+00:00)
Title: Resugar certain things in the repl, goals, etc

Well, specifically, in `showImp`. And by ‘things’, I mean ‘Nats and Listy types’.

The first patch causes anything made of `::` and `Nil` in the obvious way to be printed using the same `[a,b,c]` sugar as for input. Which I hope is a fairly uncontroversial change. :)

The second one causes `Nat`s to be printed the same as `Int`s, which might be more of a problem I suppose. I'm less sure that this is a good idea, but I threw it in anyway in case you wanted it. (BTW, so I know in future, should I have made two separate pull requests for these or would that just be clutter?) I personally don't like having `S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))` instead of `16` in my goals, but it might be a lesser evil than confusing `Nat`s and `Int`s, I dunno.