coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] overloading natural number notations for user types

From: Beta Ziliani <beta AT mpi-sws.org>
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:20:41 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:IHrGQheWc4ZSfD9y/kV4q2kBlGMj4u6mDksu8pMizoh2WeGdxc68Yx7h7PlgxGXEQZ/co6odzbGG7Oa9AidZvMbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuOOE4R2Wr1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3xap3QVfaiSMGPjg4uDXdh9B5pKdDoVe6uAc5xJTbNtLGfMFid7/QKItJDVFKWdxcAmkYWtux

On Sun, Feb 21, 2016 at 12:12 PM, Assia Mahboubi <Assia.Mahboubi AT inria.fr> wrote:

[...]
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!

[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