coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] overloading natural number notations for user types
- Date: Sun, 21 Feb 2016 17:31:15 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f172.google.com
- Ironport-phdr: 9a23:jdv7HxZmCHt78+iD4yyDljb/LSx+4OfEezUN459isYplN5qZpcizbnLW6fgltlLVR4KTs6sC0LqJ9f27EjVdsd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcCIKFwV1HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmp9sMbsrFzISRaFznoaSGQf1BRSVVvr9hb/C7X4qSz8/sVn3zKBdZn0RKszXzu46LxwGTfnjS4GM3gy92SB2Z84t75SvB/0/083+IXTeozAbPc=
How hard would it be to set up the syntax plugins already in Coq so that they registered vernaculars such as [Declare NatSyntax for nat in nat_scope [O S].] and similarly for notations for negative numbers, ascii, strings, etc?
On Sun, Feb 21, 2016 at 10:12 AM, Assia Mahboubi <Assia.Mahboubi AT inria.fr> wrote:
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hello,
Le 20/02/2016 01:08, Pierre-Marie Pédrot a écrit :
> Out of curiosity, what prevents you from writing / using a plugin?
My 5 cents: it is nice to see plugins as user-defined facilities that increase
the proof *assistant* code base of Coq.
But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.
That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?
Anyway, for what it's worth, I wrote such a plugin during last year's Coding
Sprint, with the help of Pierre Boutillier. I just cleaned it up a bit and
made it independent from its original context so that it can serve as a
documentation stub: https://github.com/amahboubi/coq-num-notations
Best,
assia
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)
iQIcBAEBAgAGBQJWydPkAAoJEFY7bbrolXGxYRoP/j1//TFFdYVPRA23mfyPuAsz
g74XI1++tqE8BPPxtuBDgm+aOGMfng1ii8/EXNSTxoJaL6N0fz9ACPCB2y//mwmU
AF0TPUJfekYb5Fu2yWaaJ3yh7IOH/4Jytxuofr9biGpWdmf+OaiZe3f9BiRoOlJc
JxMSlqVlWvTnFaiwUKtx8YcccD6XfPXS+grsX3aVK1nhyEyMYNjYkD8Ox+gnbK9d
qbDbybA9U2hzh6jbYBDjTbR99SA7XlVUndLbhXBoF6JfYJL9aIZ0wPfE4CppONNP
W+mXPz1lwQY6glvYkXmHQ5M4rHLRUCJjdtiKosTnT2iTd9dhv1v/OWcLP5ID/V0j
UPWUMEUWs0k6HMHTFROQKJzlyBG0HdZ0rqRyDYTJfEUuNgNqI8ieyfWNHeLTNIIe
z3KtqWaLj44PRp73A7f39igxeNaJJGOKPLJo4g0PmwYOEyzPWyltiOzXDlHOM70N
wiJoR2SildFUJ1T+Va2T1jWiLuKMwNtzQZS5HzB6HYkqGt9tO1UyNsuKaXLNKKfK
yV2cHPNuaPPNgC+TTA4aDP+MjBLuY8adIvXP/6vW/3GUJP7pg9y7djTZlvLM6boQ
Di2Wa3O9/jIHZ5/t5q0IiayRlYUIYuXH2nKa6pVT8oZqfKdOalw4MYVe/rRpTfPE
e7mNpbHRXVKxEARYXvbl
=t5PH
-----END PGP SIGNATURE-----
- [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/19/2016
- Re: [Coq-Club] overloading natural number notations for user types, Robbert Krebbers, 02/19/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Clément Pit--Claudel, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Assia Mahboubi, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Gregory Malecha, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/24/2016
- [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jason Gross, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/25/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Robbert Krebbers, 02/19/2016
Archive powered by MHonArc 2.6.18.