Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] difficulty computing with integers in Ltac

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] difficulty computing with integers in Ltac


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] difficulty computing with integers in Ltac
  • Date: Tue, 2 Dec 2014 00:11:11 +0100

I guess that tactics like do use "ocaml integers", and not Coq integers.

Goal True.
Definition x : nat := S O.
let N := x in do N idtac 0.

Goal True.
let N := S O in do N idtac 0.

Do not work either, and the message tells about an "integer", not a "natural number".

2014-12-01 22:22 GMT+01:00 Jonathan <jonikelee AT gmail.com>:
The following works:

Goal True.
let N := 3 in do N idtac 0.
Abort.

It produces 3 lines of "0".

So, why doesn't the following work?:

Goal True.
let N := eval compute in (1 + 2) in do N idtac 0.
Abort.

It produces the error: "Error: Ltac variable N is bound to a term which cannot be coerced to an integer.", with CoqIDE underlining the N in "do N idtac 0" as the source of the error.

How does one compute with integers in Ltac?

-- Jonathan




--
.../Sedrikov\...



Archive powered by MHonArc 2.6.18.

Top of Page