coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Custom entries examples

From: Andres Erbsen <andreser AT mit.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Custom entries examples
Date: Wed, 31 Jul 2019 14:19:00 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andreser AT mit.edu; spf=Pass smtp.mailfrom=andreser AT mit.edu; spf=None smtp.helo=postmaster AT outgoing-exchange-5.mit.edu
Ironport-phdr: 9a23:HSgi9hCPyIKfmMXkqU7FUyQJP3N1i/DPJgcQr6AfoPdwSPvyosbcNUDSrc9gkEXOFd2Cra4d0ayH7uu/AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagf79+NhG7oAXeusQUn4dpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RwgqxFvRyhuxJxzY3aYI6XNfpxYqzTctwBSGpdRclcTTBNDp+gY4YNCecKIOZWr5P6p1sLtRazGQ+sC/71yjBWnX/9wKI00/46HgHdwgMgGc8FvXPOo9XzKagSS/66zLLWwjXZdP5W3Db96JTSfh8/vP6MQKt9fMzMwkchEAPFi0+fqY3jPz6N2eQNsnSb7+p9Ve20kWIotwZxoj2py8wxiYfJnpoYxk3H+CljxIs5P8O0RU1hbdOkFJZcryOXOopsTs8/TGxkojs2xqAEtJKhYiQHx5UqywbCZ/GEaYSF5gjvWemLLTtmmH5ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrncN1wHP6siITft9/0Gh2TmW2w/N5eBLPUA0mrDdK54u3LE8j5oevV7GHi/3hEX6lrGZeVg5+uSw6uTnZKvppoOEOoNpiQzyKKAjltahDek7KAQDX2yW9fy51LL5/E35RLtKjucxkqncqJ3VP8IbqbOjAwBLyYYs9Qy/Aiyj0NQZgXkLNkxKdw+aj4TxIVHBPOj4Deujg1SriDpk2/fGPqT4DprRKnjDjazucK1m609czQoz1cpQ64hVCrEHOvLzW1X+uMbWDh8jYESIxLOtA9Jkk4gaRGinA6mDMaqUv0XCrrYkJPDJb4sIsh78LeIk7rjglylqt0UaePyA25cNZWvwM+5sOEifKS7lhNsbHHwHpCI7TfCshVGfB20AL02uVr4xs2loQLmtCp3OE9j03e6xmRyjF5gTXVhoT1CBFXCyJteDRusDbyOULYpsgjcEXL6uRsp8kxSvqEn3x6c1drOIqB1djorq0Z1O38OWjQs7pG5xDtjb3m2QHTktzzE4AgQu1aU6mnRTj1KK0Kx2mftdRI5W5u8PXwsnZ8fR

I have tried to make non-trivial used of this feature, with mixed results.
You see working examples at
https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/NotationsCustomEntry.v#L1
and non-working examples at
https://github.com/coq/coq/issues?utf8=✓&q=is%3Aissue+is%3Aopen+label%3A"part%3A+notations"+custom

Andres

[Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019
- Re: [Coq-Club] Custom entries examples, Andres Erbsen, 07/31/2019
  - Re: [Coq-Club] Custom entries examples, Emilio Jesús Gallego Arias, 07/31/2019
    - Re: [Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019