The Coq mailing list

[Tahina Ramananandro <ramananandro AT reservoir.com>]

Sorry for the duplicate. Thanks Amin for pointing to the documentation.

-- 

Tahina

On Fri, May 15, 2015 at 11:37 AM, Tahina Ramananandro <ramananandro AT reservoir.com> wrote:

(coq 8.4)

In fact, you can, the problem is not in the recursive definition, but in your use of `divide'. In your case, you should use `div' instead. If you look at their definitions and types:

Print divide.

Print div.

you'll see that (divide a b) corresponds to the predicate "a divides b", whereas (div a b) is the number (a / b) that you need here.

Hope it helps,

-- 

Tahina

On Fri, May 15, 2015 at 11:20 AM, 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?

--

Tahina Oliver Ramananandro, Ph. D.

Senior Engineer, Advanced Compilers and Formal Verification

Reservoir Labs, Inc.

632 Broadway, Suite 803

New York, NY 10012

USA

Phone: +1 (212) 780-0527 ext. 157

E-mail: ramananandro AT reservoir.com, tahina AT ramananandro.org

Web: http://tahina.ramananandro.org

--

Tahina Oliver Ramananandro, Ph. D.

Senior Engineer, Advanced Compilers and Formal Verification

Reservoir Labs, Inc.

632 Broadway, Suite 803

New York, NY 10012

USA

Phone: +1 (212) 780-0527 ext. 157

E-mail: ramananandro AT reservoir.com, tahina AT ramananandro.org

Web: http://tahina.ramananandro.org