The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can do something silly like:

Tactic Notation "mydo'" int_or_var(x) tactic3(tac) := do x tac.

Tactic Notation "mydo''" constr(x) tactic3(tac) :=

  idtac;

  match x with

    | 0 => mydo' 0 tac

    | 1 => mydo' 1 tac

    | 2 => mydo' 2 tac

    | 3 => mydo' 3 tac

    | 4 => mydo' 4 tac

    | _ => fail 1 "number" x "too big"

  end.

Goal True.

  let N := eval compute in (1 + 2) in mydo'' N idtac 0.

(note that mydo' will give the same error message as "do", so it's probably also an int_or_var)

Alternatively, you can write an ocaml plugin to convert a constr to an int_or_var. 

As to your question...maybe ltac variables or nat-interpretations are duck-typed, and so it's whatever you want it to be?

On Mon, Dec 1, 2014 at 4:22 PM, 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