coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] singleton_class_definition leading ">"

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] singleton_class_definition leading ">"
Date: Sun, 13 Jun 2021 13:22:51 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f53.google.com
Ironport-hdrordr: A9a23:R2KM+ailcnXWRREu/zTNBGkylHBQXusji2hC6mlwRA09TyX+rbHUoB17726NtN91YhsdcL+7Scq9qB/nhPxICOoqTM6ftWvdyQyVxehZhOOIowEIcxeeygc379YFT0ERMqyUMbG4t6rHCcuDfurIDOPpzEnRv5a5856ld29XV50=
Ironport-phdr: A9a23:g9LduBCA2TtKwjHMWnbkUyQU40MY04WdBeb1wqQuh78GSKm/5ZOqZBWZuaw8ygSTBs6DsbptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uyv/5DfeQtFiCSzbL99MBm6sxjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA38G/ZlNF+gqFcrh2uuxNxzJXZYJ2XOfdkYq/QZ88WSXRHU81MVyJBGIS8b44XAuYPP+ZYqI/9p1oNrRSgAQmjGv3gxyRHhn/zx6I60uAhHRva0wwnGtICvmnfodL3NKcVV+C1zarIwivHb/xIxzjw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtIPqMS+P2OsXr2ib8/RvVfipi2M/qw99vjihy9osh4TXho8YzlHJ+CplzIopKtO1TE12bMKqHZdOuC+XNZd6Tt8jTm12tys31rILtJGncCUL1pgq2hjSYOGJfYiP5xLsTueRITFgiXJkfrK/nRey/lK6xu3yTMm51ktBoCldktTUqHwByxje5tKER/Z95EutxyuD2gTJ5uxEL004jbTXJp89zrItk5cfrEDOETPzlUj5jaKaalko9+2m5unmf7rro5uROoB7hw7lN6khhNawAeo2MgULUWiU5/qw26Dm8EHnT7hFlP47n6/Eu57AP8sbvLS2AwpN34Yj9Rm/CzCm3cwdnXYdLVJFfAuLj5H3O13TOfz4A/eyjlq2nDdkwPDGObLhApHTIXTZjLjherN951ZdyAo1099f+4pZBq8dLP/3QEP8t9zVAgUnPwCpx+vrEtVw240GVWKKGKCZMafSsVGS5uIoJumBfI0VuDH7K/gk5P7hk3s5lkEDcqSy0psXbWq3HvViI0mDfXXshdIBHX8QvgUiVOzqlEGCUTlLanmuWKI8/yg3B56iDYfeXY+gm6eB3Se+Hp1OfG9KEFGMEXHyd4WFQfgAciySItUy2gADALOmUsoq0Qyk/FvxzKMiJe7J8AUZs4ji3Z57/buAuws18Gk+DcOb0mKAS2x5tmwNTj4ymqt4pAY1nlWE16l7jvhVGPRc4vpIVkExMpuKnL8yMMz7Rg+UJoTBc12hWNjzWVnZq/o+xtYPZwB2HNDw1ngrMAKlBrYUk/qAA5lmq8o0PlD0Lsd5jm/Yjewv0gJgTcxIOmmrwKV48lqLb7M=

In the Typeclasses section of the refman, a singleton_class_definition
can start with an optional ">". What does that ">" do?

https://coq.inria.fr/refman/addendum/type-classes.html#grammar-token-singleton_class_definition

[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