The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I'm trying to get [where] notation working in [Record]s.  If I do 

  Record foo := {

    Obj : Type;

    Times : Obj -> Obj -> Type;

    Foo : forall A B : Obj, A * B where "A * B" := (Times A B)

  }.

or

  Record foo := {

    Obj : Type;

    Times : Obj -> Obj -> Type;

    Foo : forall A B : Obj, A * B where "A * B" := (Times A B) : type_scope

  }.

Coq tells me "The term "A" has type "Obj" while it is expected to have type 

"Type"."

If I do

  Reserved Notation "A *** B" (at level 70, B at next level, right associativity).

  Record foo := {

    Obj : Type;

    Times : Obj -> Obj -> Type;

    Foo : forall A B : Obj, A *** B where "A *** B" := (Times A B)

  }.

then Coq tells me "Error: Unknown interpretation for notation "_ *** _"."

How can I get this working the way I want to?

Thanks.

-Jason