The Coq mailing list

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

Hello everyone:
  I was stuck when I thought about the following question:
  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.
  I define the binary  as following:
  Inductive bin : Type :=
  | O : bin
  | tw : bin -> bin
  | tw_one : bin -> bin .
  Now I want to write a function to convert natural numbers to binary
numbers,but I have no idea.Could you give me any advice?