The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Hi,

You can define bin_to_nat. You should use div instead of divide. div : nat -> nat -> nat is the division function (what you want) while divide : nat -> nat -> Prop is the divisibility predicate. i.e., "divide a b” is the logical statement “a is divisible by b”.

Take a look at the documentation of “Coq.Numbers.Natural.Peano.NPeano” at https://coq.inria.fr/library/Coq.Numbers.Natural.Peano.NPeano.html for more details.

Regards,

Amin

On 15 May 2015, at 17:20, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

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?