The Coq mailing list

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

Le Thu, 20 Dec 2012 11:54:08 -0500,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

> Maybe I'm missing something, but, the way I read the question, the
> (very straightforward) solution is to use this function:
> 
> Fixpoint div2 (n : nat) : nat :=
>    match n with
>      | S (S n') => S (div2 n')
>      | _ => O
>    end.

In the original mail, it was question of halfing to be able to
translate from nat to a binary representation. So even/odd information
is also relevant.

> On 12/19/2012 11:29 PM, AUGER Cédric wrote:
> > Le Thu, 20 Dec 2012 04:17:21 +0100 (CET),
> > "fengsheng"<fsheng1990 AT 163.com>
> >   a écrit :
> >
> >    
> >> when I wrote a function to convert natural numbers to binary
> >> numbers,I met a problem:how to take the value of a number half.
> >>      
> > [...]
> > Fixpoint div2 (m n:nat): nat*bool :=
> >   match n with
> >   | O =>  (m, false)
> >   | S O =>  (m, true)
> >   | S (S n) =>  div2 (S m) n
> >   end.
> >    
>