The Coq mailing list

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

2016-05-04 14:45 GMT+02:00 Ralf Jung 
<jung AT mpi-sws.org>:
> And while I am on it -- what is the reason that this syntax can be used
> only for implicit arguments? I think it would be just as useful for
> explicit arguments; for example to give arguments in a different order,
> or when applying a lemma, as in [apply (lemma (arg:=foo))], without
> having to specify [arg] as implicit.

It is possible actually:

Lemma foo n (P Q : Prop) : n = O -> Q -> P -> Q.
Proof.
  intros H H0 H1.
  auto.
Qed.

Print Implicit  foo. (* no implicits*)


Lemma trying : False -> False.
Proof.
  apply foo with (P:=False)  (n:=0) .
  Undo.
  Fail apply foo with (P:=False). (* fails because n should be given
if Q is given *)
  eapply foo with (P:=False). (* OK *)

Qed.

P.

> Kind regards,
> Ralf