The Coq mailing list

["fengsheng" <fsheng1990 AT 163.com>]

Consider a different, more efficient representation of natural
    numbers using a binary rather than unary system.  That is, instead
    of saying that each natural number is either zero or the successor
    of a natural number, we can say that each binary number is either

      - zero,
      - twice a binary number, or
      - one more than twice a binary number.

Inductive bin : Type :=
  | O : bin
  | tw : bin  -> bin
  | tw_one : bin  -> bin .

Fixpoint div2 (m : nat){struct m} : nat :=
 match m with
 | S (S n) => S (div2 n)
 | _ => 0
 end.

When I define the convert_bin,Coq give a message : Recursive call to
convert_bin has principal argument equal to "div2 n" instead of "n".

Fixpoint convert_bin (m : nat){struct m}: bin :=
  match m with
  | 0 => O
  | S n => match evenb n with
           | true => tw_one (convert_bin (div2 n))
           | false => tw (convert_bin (div2 n))
           end
  end.