The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Jason,

  you have to declare it before Foo is parsed:

  Record foo := {
    Obj : Type;
    Times : Obj -> Obj -> Type where "A * B" := (Times A B) : type_scope;
    Foo : forall A B : Obj, A * B 
  }.

-- Matthieu

Le 28 juil. 2012 à 15:22, Jason Gross a écrit :

> 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