The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

Hello Jason,
that should work with the "and" keyword:

  Record MonoidalCategory := {
    UnderlyingCategory :> SpecializedCategory morC;
    TensorProduct : SpecializedFunctor (UnderlyingCategory *
UnderlyingCategory) UnderlyingCategory where "A ⊗ B" := (TensorProduct (A,
B)) and "A ⊗m B" := (TensorProduct.(MorphismOf) (s := (src A, src B))
(d := (dst A, dst B)) (A, B));
  }.

-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Monday 30 July 2012 01:51:38 Jason Gross wrote:
> Hi,
> Is it possible to define multiple notations using the same record field
> with [where]?  That is, can I do something like
> 
>   Local Reserved Notation "A ⊗ B" (at level 40, left associativity).
>   Local Reserved Notation "A ⊗m B" (at level 40, left associativity).
> 
>   Let src (C : SpecializedCategory morC) s d (_ : Morphism C s d) := s.
>   Let dst (C : SpecializedCategory morC) s d (_ : Morphism C s d) := d.
>   Record MonoidalCategory := {
>     UnderlyingCategory :> SpecializedCategory morC;
>     TensorProduct : SpecializedFunctor (UnderlyingCategory *
> UnderlyingCategory) UnderlyingCategory where "A ⊗ B" := (TensorProduct (A,
> B));
>     TensorProduct' := TensorProduct
>       where "A ⊗m B" := (TensorProduct.(MorphismOf) (s := (src A, src B))
> (d := (dst A, dst B)) (A, B));
>   }.
> 
> but without defining [TensorProduct']?
> 
> Thanks.
> 
> -Jason