coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] singleton_class_definition leading ">"

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] singleton_class_definition leading ">"
Date: Sun, 13 Jun 2021 12:03:01 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f176.google.com
Ironport-hdrordr: A9a23:QsY45KyZ1W5wYrFfI89PKrPwFb1zdoMgy1knxilNoH1uA7WlfqWV9sjzuiWE7Qr5NEtQ++xofZPwIk80lqQV3WByB8bHYOCOggLBR72Kr7GD/9SKIVyYygcy79YHT0G8MrHN5JpB4PoSLDPWLz/o+re6zJw=
Ironport-phdr: A9a23:oofz2xeqA+iVLVP96rPsFLf6lGM+sd7LVj580XLHo4xHfqnrxZn+JkuXvawr0AaYG96BsLkd0beempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgFFiCCzbL9sIhi6ohjdutcWjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/jKxZrxyhqRJxwJPabp+JO/dlZKPRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt43zp1oLrRCjBQejGuPvyiVMhnDowKY31OYhEQDD3AA6EdIBrnTUrM/xNKgMSu21w6zIwi/Cb/NSwzvy9I/IchU4rPyKQLl/ftbfx1M1GAPZklWft5blPzWN2+oDs2WV4eRuWO2ghWAoqwx9vySjy8kyh4fGiI8Y1F7J+DlnzYs7O9G1VUx2bNGqHZZetiyUN5Z6T98iTWxppSo3zKANt52jfCUS1pgr2xrSZ+aEfoWI+B7vSeecLDZiiH54er+yhhC/+lW6xOLmTMm7ylNKozJFktbSsnAN0ATe6s2dRft8+ketwDeP1wTO5u1dL0A4iKjWJp87zr4/kZoTtkvDHivol0nskKCWcUAk9vCp6+ThfLrmuoeRO5Fohgz6KKgjmcyyDf4lPgUPXmWX4/mw2b/i8EHhRbVFlPw2kq3XsJDAIsQbo7a0Aw1U0oYm8Rq/ASmp0NQCnXkDMl1IYx2Hj43zNFHPJPD0F+uwg1OpkDtz3fDJIqXhAonRLnjEiLruYbF961dFxAUvydBf+olbB6oaIPPzX0/xrMbXAgU4Mwyy2ebnCc9y2pkQWWKVUeelN/bZtkbN7eYyKcGNYpUUsXDzMasL/fnr2F04nBczcKmz2ZZfPHK5G7JoLkWDZXfEjdIIEGNMtQ07Gr+5wGaeWCJeMi7hF5k34Ss2XdrO5WjrSYWkgbjH1yC+TMQ+joFuD1mNFTLpc9zBVa5TNmSdJchuljFCXr+kGddJPfSGuwrzyr4hJe3RqHVwiA==

Some clues:

The ">" corresponds to the non-terminal "opt_coercion". The text describing "record_definition" in the doc describes how that works for records.

[Coq-Club] singleton_class_definition leading ">", jonikelee AT gmail.com, 06/13/2021
- Re: [Coq-Club] singleton_class_definition leading ">", Jim Fehrle, 06/13/2021
  - Re: [Coq-Club] singleton_class_definition leading ">", jonikelee AT gmail.com, 06/13/2021