The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

What about redefining a do like tactic ?

Ltac mydo x tac :=
  match x with
    | O => idtac
    | S ?n => tac ; (mydo n tac)
  end.

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

Best,
—
Frédéric



> On 1 déc. 2014, at 22:22, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
> 
> 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
>