coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Murali Vijayaraghavan <vmurali AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Notation for Strings without double quotes
- Date: Fri, 19 Jan 2024 12:57:48 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vmurali AT csail.mit.edu; spf=Pass smtp.mailfrom=vmurali AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing2021.csail.mit.edu
- Ironport-data: A9a23:ToY7lapzco1dHVAD9WiKKPJwSw9eBmIxYBIvgKrLsJaIsI4StFCzt garIBmFOfqNZDPzf4wlPt6/9h9VsMPQy9c3TQVlqy03QnlE8uPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHoZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGjxSs//rRC9H5qyo5GtB5w1mOZingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzdFSfqV/wmWfG0YAzcmCA2k2Pq08vbd0Dlh2+ M0ICg1dNguH2uOPlefTpulE3qzPLeHsIZ8QvXBmwmuBV69gSovKQqGM4N5Emjo8m6iiH96HP ZpfMmIpNlKfM3WjOX9PYH46tPmtm2P2dzxwo0mcpK5x5mnPigF9zdABNfKMJoPUGp4EwRrwS mTu50q6IE0KaOCjyBWLznydvMTEuWTWV9dHfFG/3rsw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDScThUBq5pnHe5kRFHdFLGuw+rgSM1uzZ7xvx6nU4cwOtoecO7KceLQHGH HfQ9z8wLW0/6u+mWjiG+62KrDi/HyEQICVQLWUHVAYJqZ2r6o06khuFHJ4pHb+Xn+/FP2j64 wmLiywi2JQVr8oAjJug8X793jmDm5nuTywO3DvxYF6L1A1CSbSeV9Sa0mSDtfdkB6SFf2aFp 0kBypS/7vhRLJSjlx6tYeQqHZOr7KyrKDf33EJmL6A8xQuXol+iYoFizzVsL2h5Mss/WGHIY W2CnShz9ZNsLH+RQqsvWL2ICuMu1rnGKdTpctv2f+h+SMF9WyHf9R4/eHPK+X7mlXYdtJ0WO LCZQJ6KNmkbA6E29wiGbb4R/pFzzx9v2F6JY47wyimm9r+sZHS1b7MhG3nWZ8Ab6JK0minkw +x9BeCrlSoGCPbfZxPJ+7E9NVoJdHg3Ja7novxtK9KsHFBUJ3EDOdTwn5UaZI1Xr4ZEnLzp/ 1a8eHNi5njRuHnlETiOO1dfMO7BfJAntn8qHz0eDXDx0VgZXIufxqM+dZw2QLoZyNJe3cNEF /krR+jQA9BkaCj2xDAGXJys8K1gbEuKgCyNDQqEYR8+XYBsdzbP8IXgYzn91TYrDAeqhJAYo 7SfyR7Rfp5bYwFcD8rtSemOymmptiM3g9NCXErvI/hSdn7z8YNsFTfDs/8vL+wIKjTB3jG/1 TvKMSwHpOLInZA5wOPJiY+AsY2tNel0RWheIEX28pe0MnP80le44IodTtuNQy/RZFn09Iqme +9R6fP2a98DvVRStrtDA6RZ9r0/6/Tvto1l4FxdRluTVGuSC5RkPnWi9utMvPcUxrZm5C2Ha njW8dxeYbi0KMfpFWAKHzUcb8OB6Oo1nwfD5vFkMWT44y5KpIC8a3twBCXVqiJhL+pSCrgHk MMBo88d7jKthiU6auimij9mzEXSD3gifZh+iLQkLt7Ftg4ZxGtGQ6TgMQ7twZTWa9xzIkgge TCVo6zZhoVj/EnJclttNH3rz9tigY8qvUlSwHRfI2app9vhrd001S137j4YYFl0zBJG8uQrI UltFRR/Cpuv9gdSpvpofj6TCSAYIzPB4W336V8CtFOBfnmSTmaXcVEMY7eczn4W40d3X2Z9/ ojB7E3HTDyzXsX6/hVqaH5fs/a5EOBArFzTqvuGQfaAMYIxOwf+o6mUYmENlRvrLOUxiGDDp sho5OxAUrL6BwFBv5wED5Sm6ppIRCCmPGBiRdRTzJENF0zYexCw3mGqAGK1ccVvOffL0BGZD +pDG8FxbCm9hR2+9m0jOa0xIrFKxa9joJJIf77wPmcJvoeOtjcj4tqa6iH6g3RtWNl019o0L oTKbT+ZD2iMnj1ulnTQqNVfcH+NCTXeiNYQAMjumAnIK34CjA2oWUYvzrSzvnOaalM9plSfp wrCY+nTzvAkxIhx92cp/mOvGC3sQe4flszRmOxwjziKRdjUOMbK8QYUth/qMxk+0X45RYFsj brU2DLo9BqtgVv1Olw1X7GKDKBI4YO3XfYRP87qRJWfce1uR+e0iyY+F6uExVClXT+TCgRLh +d1VSdoSeMoZg==
- Ironport-hdrordr: A9a23:suzdWqv+8XX15HzHYhTPBBPq7skDXNV00zEX/kB9WHVpm62j5q aTdZEgviMc5wxhO03I9erhBEDiexLhHPxOkOws1N6ZNWGN1VdAR7sSibcKrQeQfBEWNdQw6Y 5QN4Z7AN30SX5gjcj75wG8V/It2sOO/qztpcq29QYOceinUc5dBs5CZDqmLg==
- Ironport-phdr: A9a23:qADlsRxAHnZSkxPXCzL7wFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hyZv6U1xwaSAs3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYAhEniSxbLBuI Bm5sAncuMsbipZ+J6gszRfEvnRHd+NKyG1yIl6dgwjy7dqq8p559CRQtfMh98peXqj/Yq81U 79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+7 6puVRTlhjsLOyI//WrKjMF7kaBVrw+7pxFnzIHaYI+bOvljcK3DYdwXXnBOUtpLWiFbHo+wc 4kCAuwcNuhYtYn9oF4OoAO5CwmxHuPg0DtIhn7r1qI10uQhExvJ3Qw6ENIUqnvUo9X1O70MU e+vyqnD0DLOb+1T2Tfg8ojHaBQhofCXUL1sasre00gvFwffglWVqIzlIymZ2foQvGiG9udtU /+khGE7pQ9ruDev2tsshZfThoIT0l3J9Th1zYQ0KNGlRkN2Yt+pHYdQuSyGNoZ6XscvT39ot Ssk1LALt4K2cicWxZooxRPSd/2Kf5aM7xzjW+ucLzN1iXR4c7y8nxa/6VWsxvP/W8Wu3ltGs jBJnsfWun0P1BHf8taLRud580u72juC1xrf5vxFLE02j6bWK5Asz7gtnZcNtUTDAzT2mFnog 6+Ma0sk++mp5Pr/b7n6oJKXKpV6hRvkMqs0n8yyGeQ4PRYKX2ic4em806Dj/VH2QLVNj/02l KbZvI7GKcgFu6K1GRNa0p055Ba+CzeqytEYnXgbLF5fZh2IkpXpN0nPIPD+E/i/n0yhnCp1y /3FJLHsDInBImLdnLv7f7tw6FZQyA8pwtBe45JUBKsBIPX2WkLpqtzYCwI5MxauzObjCdVwz Z8RWXmVDa+YNKPeq1qI5uMzI+WWeoAapSv9J+Aj5/H1lXA5g0MSfbG13ZsLb3C1BulqL12DY XXwmtcBDXsKvg0mQeP2j12CSCdfaGq2X6Ih/T42E5mmDIfGRoC1mrONxia7HptMZmBHEF+AC 3nod5/XE8sLPSmVO4pqliEOfbmnUY4okx+05yHgzL8yC/fO8ykZ/azi1tFk7vfamhE76zVyR 5CD1nyXRmV1tmgTTj4ymqV+vQpwxkrVgvswuOBRCdEGv6ABaQw9L5OJl4SSavj3UwPFJJKST Uq+B8+hCnc3R84wxNkHZwB8Hc+jh1bNxXniGKcbwpqMApF86afAxz7pPc8o1XPbzqAljnEtW cJOMSujh7I5+gTOVMbSi0vMr6+xbuwH2TLVsmKKzG6ApkZdBRB1TL/MWXE3bVDfrNC/40LeC bKiFOdvKRNPnOiFLKYCcdj1lRNGSfPkbczZeH60knysCAygwa6QY43rfWpHhH+ETkMfmgEXu 3OHKU4zCjrJT3v2KjtoGBqvZkrt9bM7s3anVgouyArMaUR91r2z8xpThPqGSvpV0KhW8CEm4 y55Glqwxbe0Q5KJuhZhcaNAYNg8/EYP1GTXsBZ4N4ChKKYqj0AXcgB+tUfjnxttDYAInc8vp XIshA18TMDQmE1EaimR2ZHYMabeK220+RGzLaPaxxCW0dqb/LsO9OVts0/q70miEksv9Wki0 sEAiiHMoM6SSlBUDsKiNyR/vwJ3rLzbfCQnsobd1Hk2dLKxrieHwdUiQu0s1hened5bdqKCD g77VcMAVK3MYKQnnUakahUcMaVc7qkxaom4cuac0aqqFO17lTOiy2FG/MZw3l/GpE8eAqbYm o0Ixf2VxF7NSTLhll6ls+j8golFYXcXH3b5xCT5Tt00BOU6bcMADmGgJNeyz9N1isv2WnJWw 1WkAksPxM6jfRf6g0XV5QRLzgxXpHWmnXH91Dloi3QzqaHZ2iXSwuPkfR5BO2hRRWAkg02+a YSzitkbWgCvYW1L3FO74FvgzqxajK9kJmjXB0JJY277I3wqXqart7WEatJC89tx63URC7z6O xbFGvb0uFMC3jnmHndCyTxeFXnioZj/kxFgySqcIHt1sHvFaJR1zBbb6sbbQK0Z1T4HSS9kz DjPUwHmb5/ypZPO0ciT4YXcHyq7W5ZecDfm19aFvSq/vyhxBAGn2uq0kZvhGBQ71iny059rU z/JpVDyeNqOtezyPOR5c01vHFK55dB9H9Q0jI4tnpgU2FARnZyU+TwCkHu1PNlGk/GbDjJFV XsQztjZ7RKwklNmM2iAw4PRXW6Uw88nYtimJG4ax2huiqICQLfR57tCkyxvp1O+pg+Eevlxk AAWzv424WIbieUE60I9iz+QCbcIEQxELDThwl6WusumovwdNwPNOfCgkVBzlte7APSerxFAD TznL4w6E3Y4790jYguWgDuosse8PoGXNI9btwXIwU6QybILbsp3zr1T208FcSr8pSF3kr591 kUohdfi+9HZY2R1oPDgWE4ea2ezP4VLvWizxadGwJTMgdj0TMk5QjxZDtyzF7qwDChasOSCV U7GETs3rmqXFOjaHBPZ5Ut752TGF5ThX52ODF8ey9gqBByUJUgFxRsRQC1/hJkyUAaj2M3md k59oDEX/F/x7BVWmKpuMFHkX2HTqR3NCH98QYWDLBdQ8gBJ5lvEec2Y4OVpGihE/5qn5AWTI 22fbg5MACkHQEuBT1zkO7Cv45HH/Y36TqKmKODSZLyVteFEf/CV2Z2o041ppW7Wb4OEJXBjC 7s+21YFUHxkWozYlzgJVy0LhnfNYsqc93LesmV8qsGy9uiuWRq6vNHfTeAKd48ppEDl5MXLf /Sdjyt4NztCg5YFxHuSjaMawEZXkSZlMT+kDbUHsyfJCqPWgK5eSRABOEYRfINF6bwx2g5VN IvVkNTwg/Rmi+MvAlNEfVf6k8CtI8kLPyewOE6NVyPpfPyWYCbGxc36e/b2UbpLkOBdrAG9o x6cDlPsOTWFmGOxDUnpOvpFjSXdOR1C/oyxb1w+bAqrBMKjYRq9PthtiDQwyrBhnXLGO1kXN j1kel9MpLmdhcu5qvJiB2NG73xqd7HewmCS9ODZLtATsOctDyhpxboyCJESwKBc7SUCQf1p3 ibes4w2y7lJuuKUwztjFh9PtnBGiJ/Z5C1f
- Ironport-sdr: 65aae261_pU3RrUUc8GDEtdMvB7NsUutuHDDFF71ZlzY3vqwzwOnBuEq fNOW55yDcbHv13rsjm9cYlu9Vxjn2d7LQbkTZMA==
Hi all
Is it possible to declare a string without double quotes? For instance, I want:
Notation "'Foo' literalString" := (Bar "literalString"%string) (at level 20).
(* Foo 25 = Bar "25". *)
(* Foo xkcd = Bar "xkcd". *)
Thanks
Murali
- [Coq-Club] Notation for Strings without double quotes, Murali Vijayaraghavan, 01/19/2024
Archive powered by MHonArc 2.6.19+.