coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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\...
- [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/01/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Cedric Auger, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jason Gross, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- RE: [Coq-Club] difficulty computing with integers in Ltac, Georges Gonthier, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Hugo Herbelin, 12/03/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Pierre-Marie Pédrot, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Gregory Malecha, 12/02/2014
- RE: [Coq-Club] difficulty computing with integers in Ltac, Georges Gonthier, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Frédéric Besson, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
Archive powered by MHonArc 2.6.18.