The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

The following message is a courtesy copy of an article
that has been posted to gmane.science.mathematics.logic.coq.club as well.


Ian Lynagh 
<igloo AT earth.li>
 writes:
>  Reserved Notation "a &&& b" (at level 50).
>  Record And (A B:Prop) := {
>     foo : Prop -> Prop -> Prop
>         where "a &&& b" := (foo a b);
>     conj : A -> B -> A &&& B -> Prop
>  }.

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