Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Hi Pierre-Yves,

Many thanks for your help. Three questions:
1/ is there any easy way to debug this when my notation is more 
complicated than the example I gave?
2/ should I put explicit coercions everywhere, or is there a more gentle 
workaround? (for instance, I don't see any such coercions in MathComp 
notation, but maybe I missed something?)
3/ any simple explanation why notation and coercions don't play well 
together?

Best,
Xavier

Le 19/09/2018 à 15:30, Pierre-Yves Strub a écrit :
> Hi,
>
> I'm very bad at Coq notations, but I think this is coming from coercions:
>
> Notation "[ x 'eq' y 'eq' z ]" :=
>     (is_true (x == y) /\ is_true (y == z)).
>
> Variable V : eqType.
> Variable x y z : V.
>
> Check [ x eq y eq z ].
>
> Best. Pierre-Yves.
> Le mer. 19 sept. 2018 à 15:19, Xavier Allamigeon
> <>
>  a écrit :
> > Hi all,
> >
> > I've got an issue with user-defined notation which, as far as I noticed,
> > only appears if the notation relies on MathComp ones. The problem is
> > that the notation is not printed as it should be (in fact it's directly
> > substituted by its definition).
> >
> > Here's an example:
> >
> > Notation "[ x 'eq' y 'eq' z ]" :=
> >     (x = y /\ y = z).
> >
> > Variable T : Type.
> > Variable x y z : T.
> >
> > Check [ x eq y eq z ].
> > [x eq y eq z]
> >     : Prop
> >
> > So far so good, the notation is printed in the correct way. Now compare
> > this with the eqType counterpart of the notation:
> >
> > Notation "[ x 'eq' y 'eq' z ]" :=
> >     (x == y /\ y == z).
> >
> > Variable T : eqType.
> > Variable x y z : T.
> >
> > Check [ x eq y eq z ].
> > x == y /\ y == z
> >        : Prop
> >
> > Any explanation?
> >
> > Best,
> > Xavier