Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] User-defined notation: bad pretty-printing

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] User-defined notation: bad pretty-printing


Chronological Thread 
  • From: Pierre-Yves Strub <>
  • To:
  • Cc: Ssreflect <>
  • Subject: Re: [ssreflect] User-defined notation: bad pretty-printing
  • Date: Wed, 19 Sep 2018 15:30:20 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:c7Bz5BdLEM0KZH5jniBbUBLrlGMj4u6mDksu8pMizoh2WeGdxcu4ZR7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM2/2/Xhc5wgqxVoxyvugJxzJLbboyOKPp+Z7nQcc8GSWZdXMtcUTFKDIOmb4sICuoMJfxWr4jjqFsUtxuxGxCgC+HxyjBWnX/9wLA00/g7EQHbxwMrAtUDsGzVrNrrLqcSS/66wLDIzDXdcfxWwizw6JPUchA7vPGDRqh8cczMyUQ2EQ7Ok1aeqZT9Mj+LyugAt3KX4ulgWO61lWIrtgJ8riKgy8syjITCm5gbxUre9SpjxYY4Pd24R1B/Yd6jCJZQsjuVN4pyQs87RGFouTo2xqQIuZO0YiQG0psnxxnYa/yId4iH/AjvW/qWITd9nH5lebS/iAiu8UW41OHwSs253ExJoydFiNXAqG0B2h/J5sWIVPdx5kKh1iyO1wDX5OFEO0c0la/DJp45w74/iIATsV7dESPvmET2krGZdl4/9+iz9+TneKjmqYSGO49ylwHyKr4uldCnAeQkLggOWHCW+f+n1L3540L5TrFKgeMqnanFq53aPsQapquhAwBPyIoj6hC/Dy2n0NsCh3UHIkhFK1q7iN35Mk/PLeq+BPO7ilGtnzpswdjHOKfgC9PDNCvtirDkKI585lRGxU8C091Er6lIEKwLaKbrW0LrrtGdHwE0KCSv3/z6ApN7y9VNCiq0HqaFPfaK4hez7eU1LrzUPd5HiHPGM/EgosXWozo8kF4Zc7Ou2MJPOmukBOlsZUOEMyO13oUxVFwStw97d9TEzUWYWGcLNW2uRb82oDcmWtr/UNXzA7u1ibnE5x+VW51bYmccVwKJGHbsMoKFA7ICNHjULchmnTgJE7OmTt152A==
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

Archive powered by MHonArc 2.6.18.

Top of Page