Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Convert nat to binary

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Convert nat to binary


Chronological Thread 
  • From: "fengsheng" <fsheng1990 AT 163.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Convert nat to binary
  • Date: Tue, 16 Jul 2013 06:48:46 +0200 (CEST)

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?




Archive powered by MHonArc 2.6.18.

Top of Page