coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] overloading natural number notations for user types
- Date: Sun, 21 Feb 2016 19:18:48 -0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=None smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT famaf.unc.edu.ar
- Ironport-phdr: 9a23:/UmcFBdruYyyMasN99ba/2gRlGMj4u6mDksu8pMizoh2WeGdxc69Yh7h7PlgxGXEQZ/co6odzbGG7Oa9AidZvMbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuOOE4R2Wr1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3xap3QVfaiSMGPjg4uDXdmM10jatdoTqvrhl2zcjJZorTOfZjOKrHK4BJDVFdV9pcAnQSSri3aJECWq9YZb5V
On Sun, Feb 21, 2016 at 12:12 PM, 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?
You mean to incorporate parsing primitives to (e.g.) Mtac? This can be an interesting project indeed!
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] 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.