The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Nicolas,

notice that this works:
  t ltac:(2).

you may define a tactic notation instead, because you can force the
type of arguments:

Tactic Notation "t" int(x) := (do x intro; idtac "stop").

It is not completely satisfying because t is not bound to a ltac
function, but to my knowledge there is no way to force the type of the
arguments of a tactic.

Hope this helps,
Pierre

2018-02-09 11:55 GMT+01:00 Nicolas Magaud 
<magaud AT unistra.fr>:
> Below are 2 tactics t and u which I expect to behave in the same way.
>
> They perform (if possible) x times the tactic “intro”.
>
> However I do not manage to run “t”. Writing "t 2. "leads to an error 
> message.
> I can still achieve my goal by writing a recursive tactic, but using the 
> “do” construct would be more straightforward.
>
> Am I missing a constr: , ltac: or something similar somewhere ?
>
> Thanks in advance
>
> Nicolas Magaud
>
>
> --------------------------------------------
> Ltac t x := do x intro; idtac "stop".
> Ltac u x := match x with O => idtac "stop" | (S ?p) => intro; u p end.
>
> Lemma f : forall x y z:nat,  x= y ->  z= y.
> Proof.
>   t 2. (* Error: Ltac variable x is bound to a term which cannot be coerced 
> to an integer.*)
>   u 2.