The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

So, I'm doing the basic exercises, and I encountered this issue:

Inductive bin : Type :=

  | O : bin

  | Beven : bin -> bin

  | Bodd : bin -> bin.

Fixpoint incr (b : bin) :=

  match b with

    | O => Bodd b

    | Beven e => Bodd (Beven e)

    | Bodd o => Beven (Bodd o)

  end.

Require Import Coq.Numbers.Natural.Peano.NPeano.

Fixpoint bin_to_nat (b : bin) : nat :=

  match b with

    | O => 0

    | Beven e => 2 * (( divide (bin_to_nat e) 2) + 1)

    | Bodd o => 1 + (bin_to_nat o)

  end.

(* Error:

Toplevel input, characters 91-114:

Error: In environment

bin_to_nat : bin -> nat

b : bin

e : bin

The term "(bin_to_nat e | 2)" has type "Prop"

 while it is expected to have type "nat".

*)

Why can't I define bin_to_nat to be recursive just as I would in OCaml?