The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon xiang sen 
<xiangsen AT ustc.edu>:

> Hi, all :
>
> When I apply a lemma on the current goal , there are many parameters
> required to be specified.
> But their order seems puzzling. What 's the mechanism of order
> determination in coq. Thanks!

Hi, Xiang,

 Have you some examples of problems you encounter ?

 In general, the order is the left-to-right order.
 Nevertheles, some little problems can arise if you are working through a
notation which permutes this order :

  Notation "x < y" := (my_module-gt y x) : my_scope.

 You must consider that y is at the leftmost position, even if
"x < y" is displayed.

 But this is not a big problem: In dubious situations, I use the
command Check or About to look at the names of the parameters, and
I use the (A:=t) feature (look at "apply with" and at "implicit parameters"


Cheers,

Pierre

>
> All the best!
> Xiang 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.