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:47:11 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:0VAsahNdQhOzAD/Tm8Il6mtUPXoX/o7sNwtQ0KIMzox0Lf76rarrMEGX3/hxlliBBdydt6obzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuxNxzpXIYIGMLvdyYr/Rcc8YSGdHQ81fVzZBAoS5b4YXFeQBPPhXr5Pnp1QQtBexBxesC/30yjRVm3H2wbc60/k6Hgrb2wEgB9MOv2rOrNXvKqgeSOC0zLfWwjXYdP5Wwiv96JLVch86u/2MW69wfNPXxEIyFA3Flk2dpZL5Mz6RzOgAsGiW4/B+We6yl2IrsQF8riSpy8wxkIfGnJgVxUrB9ShhwIY6O9m4SEljbN6hCpRQtiWaO5JxQsM+Xm1koSg6x70atZKhcygKz5MnxxHba/OZaYSH/hXjVOOJLTd5gnJqZq6/ig6s/US8zuDwTMq53VZQoiZbj9XAqmoB2hzP5sSfT/ty5Eah2TKB1wDJ7eFEJFg5lbLaK5E/2L4wjIQcvV3DHy/ohkr2l7Sbdl44+uiy9uToea/qppmBN4NskAHxLrwumtCjAeQ/KgUORHOb+f6i273t+U32XqlFjuEtn6nCsJHaINwbqbSjDw9U1IYj8Re/AC283NQWh3lUZG5CLQKOkYnkIRfHJPTxCPawjlOquDZt3fHPeLP7UbvXKX2WqLbsZ6xwrn9CxRF79sxF+pgcXqkALejpVwrgqtHDJgQlKRG+heD6XoYunrgCUH6CV/fKeJjZtkWFs7p2cru8IbQNsTO4EMALovvnjHs3g1gYJPH7xocNdXr+GOk0ehzFM0qpuc8IFCIxhiR7VPbj0QXQSiJJenz0Wb9uvmhmWrLjNp/KQ8WWuJLE3Cq/GccLNGVPC1TJFmuxMovZA7EDbyWdJsInmTsBB+Cs
Le mer. 19 sept. 2018 à 15:43, Xavier Allamigeon
<>
a écrit :

> 1/ is there any easy way to debug this when my notation is more
> complicated than the example I gave?

What I do is to set "Set Printing All" and to see if my notations is
not too restrictive by instantiated implicit arguments.

> 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?)

ssreflect/eqtype.v:Notation "{ ? x : T | P }" := (option {x : T | is_true P})

> 3/ any simple explanation why notation and coercions don't play well
> together?

I let notations experts answer this question.

Best. Pierre-Yves.

Archive powered by MHonArc 2.6.18.

Top of Page