The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 12 Jan 2013 08:16:07 +1100,
Ramana Kumar 
<Ramana.Kumar AT cl.cam.ac.uk>
 a écrit :

> You may be interested in what the HOL community calls "Norrish
> numerals". They are like binary numerals but with unique
> representations. The constructors are
> zero,
> n |-> 2n+1, and
> n |-> 2n+2.
> 


I was not aware of it. But on my side, I reinvented it.
Note that for "symmetry" reasons, I prefer:

zero
n ↦ (2×n)+1
n ↦ 2×(n+1)

which of course is exactly the same.

But as people are more used to classical binary representations, I
would advise fengsheng to use its stuff in at first, and then if he
wants to try to rewrite all with this version, which adds to the
initial difficulty another one, which is a unusual representation.