The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.

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.
>