coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] overloading natural number notations for user types
Date: Fri, 19 Feb 2016 16:52:44 -0500
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-qg0-f44.google.com
Ironport-phdr: 9a23:J28qtxxybq0TzVLXCy+O+j09IxM/srCxBDY+r6Qd0e0SIJqq85mqBkHD//Il1AaPBtWEra8cwLOK7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZnvnLnupdX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjUSrY9RTSr6e9PRR72hSEbf2o792fWicF0ga9zrxeophg5yInRNtLGfMFid7/QKItJDVFKWdxcAmkYWtux

Is there a way in Coq to overload the natural number notations? There seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a BigZ.t_. However, in neither case is the Notation "42" itself defined. At least in the case of bigZ_scope, the only notations defined are "0", "1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local. So, what magic makes it work for all other natural number notations as well? And can it be used for user-defined types?

-- Jonathan

[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