coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: generalized variables

From: Adam Megacz <megacz AT cs.berkeley.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Re: generalized variables
Date: Sun, 02 May 2010 00:09:43 +0000
Cancel-lock: sha1:11NEPQS/sPPJ+TnnWCvtRMXWEOA=
Connect(): No such file or directory
Organization: Myself

Loic Pottier
<loic.pottier AT sophia.inria.fr>
writes:
> then can one write something like
> forall `(A:part E), True
> in order to get E generalized automatically, like it works in
> arguments of  Type Classes?

Yes:

  Definition part(E:Type):= E ->Prop.

  Definition test : forall `(A:part E), True.

    intros; auto.

  - a

[Coq-Club] Re: generalized variables, Adam Megacz