The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

Ah! Thanks a lot!

But if I define splitex like this :
Ltac splitex :=
repeat match goal with
| H : ex _ _ |- _ => inversion_clear H
end.

Then
(**** Example **)

Require Omega.
Lemma ex_try:forall m,(exists n:nat, n<m)->(exists n:nat,n+2<m)->m>=3.
intros.
splitex.

splitex doesn't work.

Why ? :)

Sen


anoun AT labri.fr
 wrote:

> Hi Sen,
> Your tactic works if you use the type 'ex' instead of its notation (exists 
> _:_,
> )
>
> Ltac splitex :=
> repeat match goal with
> | H : ex _ |- _ => inversion_clear H
> end.
>
> (*very simple example*)
>
> Require Omega.
> Lemma ex_try:forall m,(exists n:nat, n<m)->(exists n:nat,n+2<m)->m>=3.
> intros.
> splitex.
> omega.
> Qed.
>
>
> Houda
>
>  
>
> > Hi , everyone :
> >
> > I used below to define a tactic :
> >
> > Ltac splitex :=
> > repeat match goal with
> > | H : exists _:_, _ |- _ => inversion_clear H
> > end.
> >
> > But it does not work. Coqtop reports :
> > Syntax error: [constr:ident] expected after 'exists' (in
> > [constr:binder_constr]
> >
> > All the best!
> > Sen
> > --------------------------------------------------------
> > 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
> >
> >    
>
>
>
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> --------------------------------------------------------
> 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
>
>
>