Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Overloaded notations in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Overloaded notations in Coq


Chronological Thread 
  • From: "Kyle Stemen" <ncyms8r3x2 AT snkmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Overloaded notations in Coq
  • Date: Sun, 04 Jun 2023 19:43:35 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ncyms8r3x2 AT snkmail.com; spf=Pass smtp.mailfrom=ncyms8r3x2 AT snkmail.com; spf=None smtp.helo=postmaster AT sneak2.sneakemail.com
  • Ironport-data: A9a23:yU9Ycas+qZ8aXuNFTBEifZJttefnVGBaMUV32f8akzHdYApBsoF/q tZmKTiBb/yPa2ryfNkjYY6//UhS68DWzd8yGlZvpStgEi5DgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMs8pvlDs15K6p4G1A4gRnDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJGY8O7IK1PQsOCZhx PZfNwxKXw66jdvjldpXSsE07igiBNLtMYoc4Dd7yzzQDvsjSJHHBa7N4Le03h9u2oYSQ7CHO ptfMGY/BPjDS0Un1lM/Dpkvmfz4nCLvKRVDrlGQrKszpWPUyWSd1ZC0aYOMIYTRHJo9ckCwv F352Uj8MEkgJdGjyRyb20OTnb+MpHauMG4VPOHgqKIy0TV/3Fc7AxoPEFC/vPORkV+7Q9sZK koO+yNoo7JayaCwZsL7UhS7+jifuBMVWNdVGuw+rgqKz8I4/jp1GEAjRDh+evI07/Zxag0gk UC12OL3PDZW5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiN1v5v4oZoo/eJNZnuEZChmrn G/X9HlWa6E7yJ9Uh//irDgrlhr1/sCRJjPZ8Dk7SY5M0++UTJWjaoWrsx7A6/tJL4ucR1iF+ nMDnqByDdzi77nSy0Rho81XR9lFAspp1hWA3TaD+LF9q1yQF4aLJ9w43d2HDB4B3jw4UTHoe lTPngha+YVeOnCnBYcuPdLsWpxxkPS7Toy/PhwxUjaoSsQtHONg1H0yDXN8I0i0+KTRufBua cvznTiEXR729piLPBLqH7lBie5DKtEWznLZSIqzxh+s3KGFLH+TVbofNlaSJus+6aaZpgTe+ speMM2Royizo8WjChQ7BbU7dAhQRVBiXMieg5UOJoarfFE8cEl/UKC5/F/UU9E/90ijvr2Wr ijVt44x4AeXuEAr3i3TMCE+Meq1B8YkxZ/5VAR1VWuVN7EYSd7HxM8im1EfJNHLLcQznaAmf OpPYMiaHPVERxLO/jlXP9G3r5VveF7vzUiCNjasKmp3NZNxZR37yvm9dCvW9Q4KEnWWs+k6q OaezQ/1e8cIaDljK8f0U8iR6W2Nk0ITot8vYHuQEOJvIB3t1KNINx3OiuQGJpBQCBfbmRqf+ QWkITYZgujvsYUw7MX4uqSfi4KPDeFFP1F7GlPD5u2cLhjq/WuEwK5BXt2XfDvbanjGxaW6a chRzND+KPcinmsWg7FjEr1u870y1+Hvq5Be0A5gOnfBNHavNZ9NPViE2pNpmpBW57oEpzazZ F2DyuNaNZqNJsnhNlwbfyghT+ab0MAriivg1us0LGr69R1I0uK+C2sKBCa1iQtZMLdRG6Emy 714uMcptiqOuiBzOdOC1i1p52CAK0IbaJoet7YYPt7PqhEqwVR8c5DjGnfIwJWQWe5tbGguA BGp3ZTnuZoN53DsUXQJEVr14dF8nrUL4RBD808DLQ+Gm/3Dnf4G4ydS+jUWECVT6AhOibtzM 1d0KnwvdLmv/ihptudHTWuDCwFMPzzH203Tmn8itnzVcFmsbUPJdFYCAOeq+FsI1V5cchxw3 qCq+Ey8XRnEJMjOjzYPA2h7oPndfPlN3wzlmvH/Of+aHpM/MAHXsoX3aUUm8xLYUN4M3mvZr uxX/cF1W63xFQgUh4YZU4C697AheCqoFVx4Y8NK3f02RDnHWTSIxzKxBVi7eZpNK9z04EaIM ZFSCfwVZSuu9hSlj249NfYXLq5WjcwZwoMIWonWKF4st5qdqTtUs6zsyBXuuV9zQ/tSvJY8D qjzawO9FnehgCoIum3V8+hBFGmKQfgFQwzezuqwzuUABbMeu7sxdXANzr++gFuNOiA6/RjO5 ALnTI3VxtxE1o5DsdbNEKJCJgPsMvL1dr2C3z6SuuR0T+HkEJnxpSYKjFj4LiJqMqA3Z+1np Y+SsdXy4lzJjIw2X0/dhZOFMatDvue2Y8Z6LeP1KyN8sRaZecqx/SYGxX+0GaZJnPxZ+MOjY QmyM+m0VNwNXuZi1G9nUDdfHzkdGpbIQP/Z/w3llMu1Cz8ZzQDjB/Gk/yWwbWhkKwk5C6enA Qrw4/uT9tRUqbpXPyA9BtZkPc5IEAe2E+9uPdj8riKRAWSUk0uP8Omq3wYp7TbQTGKICoDm6 JbCXQLzbwm2pLqO9txCrohupVcCOR6RWwXrkp41oLaaSgxWDVLq6cwGN5gPCcsSiSr/3ZL1Y TjMaC0pDiCVsfGot/njyIyLY+tdLrVm1hTFyvgB5EWXbi63AMWLB74JGuJI/SJtYjW6pA24A Yh2x5AzVyRdBrlyQ+UW7/2/x+xgw5s2A57OFV/Vy6TPPvrVPVnGOLGN0uaAuewr3vwhTHn2G FU=
  • Ironport-hdrordr: A9a23:yYMTxaPrrKhVXMBcTtKjsMiBIKoaSvp037BN7TEVdfU1SL37qy nKpp4mPHDP5Ar5NEtOpTniAtjifZq/z/9ICOAqVN/IMTUO01HJEGgN1+XfKkXbaknDytI=
  • Ironport-phdr: A9a23:hbx4dhyZ8/prnUXXCzJcwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hGZvqQyxwaSAs3y0LFttan/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys+5DfeQtFiT6/bL99M Rm7owfcvdQKjIV/Lao81hTGrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02Q aRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+8 6tmTgLjhyAZOTEn/2DXltV+jKRfoBOhvhBz2pLZbY+XOfdwZ6/RYdwXTndFUstRSyBNB4WxZ JYNAeUcJ+ZVt4fzqVsQoxW9GAejC//gxDBPiHLtwa030f4sHR3c0QA8Hd8DtmnfotXvNKcVV OC41KfEwzDDbvNSxzj29ZXGcgw/rvGJQ71wd8TdwlQoGgPDklqRqYnlPyiW2+QXvWWa4PRsW Pm0i24hqAFxpyKgxsYoioXTmo0VzVXE+Dx/zY0oKtK2VFR1bsS4EJtMqS6aLY12T9ssTWxpu Ss3xLILtYKlcSQW1Zkq2R3SZviZf4aH/B/tW/qcLCtmiX9hZL6yhRS//VavxODiWcS63kpHo y5KnNTMsH0GyhLd6s+CSvRn/0eh3y6C1w/S6uFYIUA0iLHUJ4Q9zb43k5oet1nIECzumEjuj aKbeV8o9+ep5uj9f7nrppuRO5VphgzxMakjnNG0D/4iPQgURWeb/Pyx1L398k39R7VHluY2k q/Hv5/AJsQXuLS1AxRT0ok98Rm/DCmp0NECknkGKFJJYg6Ij4/sO13WIfD4C+mwg0i0nTpqy P3KJLLsD5TXInTekLrseaxx51NTxQcw1dxf4ohbCrAFIPL9QE/xs9nYAwc/MwOow+fnDc592 4AEWW+BDa6VLrjfsUSO5uIsJumDfo4VuDLnJ/c54P7uiGc1mVkGcqaxx5sYdGi4Huh6I0Wee Xfgn88NEX0WsQomUOzqlFqCXCZPaHa1RqIw/y00CIa7DYjYXY2tm7yA3CKjHpJMfGxGC1aME W3pd4qeQfsMZjiScYddlWkPUqHkQIs83zmvshX7wvxpNLn64Cod4NjAxdx4r9bPmBQ/83Y8W 8KWwmSWH3svjjkgXDk12al+pQp2zVLVgvswuOBRCdEGv6ABaQw9L5OJkrQS47HaXwvAeo3MU 1O6WpC8Bjp3SNstwtgIakI7GtO4jxmF0TD5S6QNmemtA5o5urnZw2C3P9x0nnDNxaw630N9U pFnLmulg6d+807YAIua216BmfOSfL8HlDXI6H/FyGOPuE9CVwslV67UWGtPfBDG9/zi4EDHR r6qT78gN1gJ0taMf41NbNChllBaXLHjNdDZNnq2gHu1DA2Uy6mkd4zncmZHmj7bBUEHngUa/ HLAPg87bsu4i0TZCjEmVVfmYke2tPJ7tGv+VEg/iQeDc0xm0bOxvB8Tn/2VDf0JjPoCv286p jN4EUzYvZqeAsecpwdnYKRXYM8sqFZB22XDsgVhP5umZ6l8j18aeg5zsgvgzRJyQolHlMErq jstwm8QYeqe20JEbGOChoCqEqbRKWz7/RTpYKnTmxnf3NuQ5qYT+aEgsVyw2WPhXkEm8nhhz 5xUyy7CutOWUkxLDMO3CxpnpH0Y7/nAbyIw5p3ZzyhpOKiw6HrZ3s4xQfEiwVCmdsteN6WNE EnzFdcbDo6gMr9P+RDhYxQaMeRV7KNxMdmhcq7M3qW6Of0whmm210xc5oN420OIsSF7T6Sbu vRNi+HdxQaBWzrm2R2nudHygtBePiFINnG5yi3tBYoXbap3N9Vuay/mM4i8wdNwgIToUnhT+ Qu4Bl8I78SufAKbc1332QA4OV0/mXW8gmP4yjV1l2tsta+DxGnUxO+kchMbO2lNTW0kjFH2I IHygcpIFESvagEoklOi6yOYj+Bdr7V6NDnJGlcSVzPwLGRrU6/2vb2HK8JC85IntyxLXf/0P wzcFuC7+kZLlXq/TyNX33gjeiuvu4nlkhAf6irVN3t1oHfDOIlxyRrZ+N3AVKtU1zsCSjN/j GqfDVy9Mt+1uNSMwsmf9LzgETv8B9sKLXm4qOHI/DG27mBrHxClyvW6m9m9VBM/zTe+zd5hE yPBsBf7ZIDvkaW8K+NuOEdyVzqeo4J3HJ9zlowoidQew38f09+T9msCijfpasUB8bn4b38ER DpNyNnQqluAugUrPjeSyoT1W2/IiM1qdtyhMnlNyngV9MZJDa6V6PpPmi4/8T/a5UrBJPN6m Dka0/4n7nUX1voItAQaxSKYGrkOHENcMH+kh1GS4tu5tqkSeHe3fO36yh9lhd74RuLnwEkUS DPjd5wlByM18shvLAeGzijo8o+9MNCCdtQevx7O1QzGguFWJZc4l/5Mji1icTX0uXlvowIip Tpp25zy/I2OKmE3ubm8HgYdLDr+IcUa5jDqi69a2MeQxYGmWJt7SH0NW9PzQPSkHSh317yvP huSEDA6tnaQGKbOVQ6Z5kB8qnvTEpetf3iJLXgdxN9mSVGTPktayAwTWTw7mNY+GGXIjIT5d 1xl4zkK+lPiggBKx+trbV/kVGrWpwqtYzYwDpOYKVse7w1P4VvULd3L7u93GHI9nNXppwiMJ 2qHIgVQWD9VHBDaQQm+b//3uYmTlorQTvCzJPbPf7iU/OlXVvPSgImqzpMj5TGHcMOGInhlC fQ/nEtFR3FwXcrDyFBtA2QakTzAa8mDqVKy4Cpy+4q5++XuQ1L1vpvVI6BUMtBm+hTwiqCGf b315m4xOXND25UAyGWdgqAYx0IXgjpyeiOFCrINvC2XCrnWl6ZUAhsSaic1P8xNpfFZvEEFK YvQjdX70aR9h/g+BgJeVFDvrcquYNQDP2C3MF6v7KmjL7KFIDTKx4f8ZqbuENW4bc1PsRC5u mzdCEnuNzeOkjDoU1akNuQe1Elz2TRFvoK4exdpT2PkSYC+AiA=
  • Ironport-sdr: 647ce969_rh5s3SOjT+4PrvO6G9UEXVzELdrXsNK5AZG8Y0eWJmhndn9 EOwzMyijdh/5B/3Mew+UsTspW+X5wli2BdAT+RQ==

The existing documentation I found for how to overload notations didn't quite
match what I wanted. The approaches in the documentation were either not
flexible enough (notations bundled with properties, or doesn't support
dependent types) or not robust enough (doesn't work in a proof goal).

After a lot of trial and error I created a library for overloaded notations:
https://github.com/bluelightning32/coq-overload. It uses a combination of
type classes and canonical structures.

I'd love feedback on how to make the library simpler (while still passing all
of the tests) or more robust. Feedback on the library's documentation is also
welcome.


  • [Coq-Club] Overloaded notations in Coq, Kyle Stemen, 06/04/2023

Archive powered by MHonArc 2.6.19+.

Top of Page