[chriswarbo]

> If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them?

I don't think so, but Natural numbers can't be represented as two's-complement "integers"; neither can Integers.

There are many ways to encode such numbers if you really want; the easiest are probably "Fin (2^32)" for a type with 2^32 members (easy to convert to/from unary Naturals), or "Vect 32 Bool" for a list of 32 Booleans (easy to do bitwise stuff). You'd need to decide how to truncate the Naturals though; do you take min(x, 2^32 - 1)? Do you take x % 2 ^ 32?

Also, note that "S (S (S (S Z)))" isn't really a list; to turn it into a list we'd have to associate some trivial data with each constructor, eg. [NULL, NULL, NULL, NULL].