coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] natural numbers as a datatype and as decimal numerals

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 16:24:26 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f48.google.com
Ironport-phdr: 9a23:RSWxFx3sQEJPerYLsmDT+DRfVm0co7zxezQtwd8Zse0TIvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycYsPCPAGPelArIb9pl4OrR6gCgm2AePg0DlIhnnr1qA9z+QhER/J3As6E9MPsXTUqdD1NKYJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrx+dsrRzFMgFwLDjliIpozlODSV1usJs2eF9eZvSeWvi2s/pwFwpDiv2tkjio3Tio0I1F/J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTm9ytCs1ybALv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOTJ4i2hkeLK7nhqy70ugxvHlWsm631tHrTBJktbLtnAK2BzT7taIRuFh8Uem3DaDzwHT6udaLkAojafXNYItz7oqmpcQsUnPBDH6lFj4gaOMeUgp+fCk6+H9bbXnop+cOZV0igb7Mqk2hsy/Afo3Mg8UU2ma+OS80bjj/UziTbVFi/05iKjZsJTAKcsHoa65BhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxltrnidJK5IIbXG+VB6afNuuGrV+F4aQ9IuyJZacavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkzexzIM0qpuc8IFCIxhiR7SeXrjFOYVjsKPiS9Wqs94ncwD4f0VN6fFLDou6SI2WKAJrMTfnpPUwneHnLhdoHCUPAJOnrLf51R1wccXL3kcLcPkBGjsAigluhiJ+vQvzMb7dftiIgz6OrUmhU/szdzCpbF3g==

I don't think there are anything planned for strings yet but feel free to open a feature request if you think that would be valuable ;-)

Le lun. 14 mai 2018 à 16:11, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Théo,

Interesting! One question: is there also something planned for quoted character strings? These are also somehow “magically” converted to Coq string objects. It might be interesting to convert strings to arbitrary objects with a parsing function depending on scope in a similar way as numbers are converted in the PR you mentioned. E.g. the Software Foundations “ImpParser.v” shows how to parse strings with simple programs to data structures. Since Menhir can generate Coq parsers (Afaik) this might be a powerful feature.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] natural numbers as a datatype and as decimal numerals, Gergely Buday, 05/14/2018
- Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, David P Á, 05/14/2018
  - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Gergely Buday, 05/14/2018
    - RE: [Coq-Club] natural numbers as a datatype and as decimal numerals, Soegtrop, Michael, 05/14/2018
      - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Théo Zimmermann, 05/14/2018
        
        RE: [Coq-Club] natural numbers as a datatype and as decimal numerals, Soegtrop, Michael, 05/14/2018
        
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Théo Zimmermann, 05/14/2018
        
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, José Manuel Rodriguez Caballero, 05/14/2018
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Gaëtan Gilbert, 05/14/2018
        Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Maxime Dénès, 05/14/2018
    - Re: [Coq-Club] natural numbers as a datatype and as decimal numerals, Li-yao Xia, 05/14/2018