The Coq mailing list

[megacz AT cs.berkeley.edu]

Thank you Ian!  That's exactly what I wanted.  One more question: where
do I place the "where" clause if the Notation uses identifiers which are
parameters of the Record?  For example, rather than write this:

 Record Foo (func:Type->Type->Type) :=
 {
   pf     : func Set Set = Set
 }.

I would like to write

 Reserved Notation "a ~> b" (at level 30).
 Record Foo (func:Type->Type->Type) :=
 {
   pf     : Set ~> Set = Set
 }.


AUGER C??????????????????dric 
<Cedric.Auger AT lri.fr>
 writes:
Your example is quite strange for defining the And; I would rather do:

Yes, the example I posted was completely artificial.  The real case I
have in mind is very large and I didn't want to make people read through
the whole thing just to answer my question.

 - a