The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

Hello,

What you need is tactic notations described in Part III of the
reference manual. They have the same relationship to tactics as
ordinary notations have to terms.

You can write your code as follows:

Tactic Notation "mydestruct" constr(o) "as" simple_intropattern(x) :=
destruct o as x.

Definition test : list nat -> list nat.
intros x.
mydestruct x as [|head tail].

As you see, every word in the notation either has to be enclosed in
quotes, which means that it appears literally when the tactic is
invoked, or it represents an argument whose "type" must be provided.
For more examples of tactic notations, search the Coq distribution. In
particular, the file test-suite/success/ltac.v contains some examples
with argument "types" not mentioned in the table at the end of chapter
11 of the reference manual.

Yevgeniy

> On 4/5/07, Sean Wilson 
> <sean.wilson AT ed.ac.uk>
>  wrote:
> > Hi,
> >
> > I have a simple query about using Ltac. I'm trying to write a tactic which
> > makes use of "destruct" and want to be able to name the new variables
> > introduced into the context e.g. "destruct x as [|head tail]" instead
> > of "destruct x". I tried this Ltac tactic:
> >
> > Ltac mydestruct o x := destruct o as x.
> >
> > But it doesn't work:
> >
> > Definition test : list nat -> list nat.
> > intros x.
> > (* mydestruct x [|head tail].  (* doesn't work *) *)
> > destruct x as [|head tail]. (* works *)
> >
> > How do I say in Ltac that "x" should be an introduction pattern? Also, are
> > there any good sources for answers to questions like this about Ltac?
> >
> > Regards,
> >
> > Sean
> >
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >