coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] Convert nat to binary, fengsheng, 07/16/2013
- Re: [Coq-Club] Convert nat to binary, Casteran Pierre, 07/16/2013
Archive powered by MHonArc 2.6.18.