[Agda] termination

[Permjacov Evgeniy]

On 03/03/2011 02:45 PM, Conor McBride wrote:
>
> suggest that solving the
> slightly more general problem of addition-with-carry might give you a
> cleaner solution, because it has a neater, more compositional structure.
>

Ok, it is very possible. However, the problem is, that I does not know
so much about math. I'm neither computer nor math scinentist. So, I wish
to ask you, what do you mean?

I think, I have to declare reason, why not to use simple church encoding.

The church encoding, i.e. one with
data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

is intuitive and effective for reasoning about numbers themself.
However, the main representation of numbers in computer is one using
binominal encoding, with fixed or variable length of bit sequence. So,
to reason about numbers in computing, one need bitwise encoding. And
this is the only reason to use more complex enconding than Church one.