Yes, I have been reading Okasaki ...
What do you mean, it's computationally foolish to define arithmetic using the Peano axioms?
>pinc [] = [1]
>pinc [1] = [0,1]
>pinc (0:u:xs) =
> if (head (pinc xs) == 0) then (u+head (pinc xs) : drop 1 (pinc xs))
> else (u : pinc xs)
>pinc (1:t:xs) = 0:t+1:xs
>pinc (u:xs) = 0:1:u-1:xs
>pnums = iterate pinc []
>pinc [] = [1]
>pinc [1] = [0,1]
>pinc (0:u:xs) =
> if (head (pinc xs) == 0) then (u+head (pinc xs) : drop 1 (pinc xs))
> else (u : pinc xs)
>pinc (1:t:xs) = 0:t+1:xs
>pinc (u:xs) = 0:1:u-1:xs
>pnums = iterate pinc []