Ssreflect Users Discussion List

[Xavier Allamigeon <>]

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