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: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 14:10:49 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:JFmLtRSHFCKJT+QlAdIRDCjLV9psv+yvbD5Q0YIujvd0So/mwa6yYRSN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO+FzcbnBcd4eX2dNQtpdWi5HD4ihb4UPFe0BPeNAooXzulUOqgWxBQawBOP1zT9Inmf61rA93eQgDQ7G3BYvEMwKsHjasd74M6ISUeGpw6nI1zrMcfdW1S3m6IjPbB8hru2MXah3ccrJ0kQvFgXFjkmOpozhJT+ayuMNs22C4udmSOmhhWknqwRrrTiuwMchkojJhoQJyl/a8SV12ps6KsO+RUVmYtCkCINduzyUOoZ5WM8uXm9ltSkgxrEbt5O2fTIGxIooyhLHdvCKcoaF7gjtWeufOzt0mnxodbalixqv8kWs1vXwWtS13VtOtCZJjNnBu38X2xDN8MSLVPRw80On1D2SzQ7c8PtELloxlafDK54u3Lowlp0LvETGES/5gln6gauMekUl/Oio9/roYrH8qpCAMI90jxnyMqUomsOhHeQ1KhUCUmaU9OimybHu80L0TK9XgvA4k6TVqo7WKMsDqq68GQBV04Ij6xilDzeh1dQVhXwHLFNZdxKHlYfmJVXOLOrjDfe4nVusnytrx+rBPr35GZjNL37DkKv/crZ58UJT1A0zzdVH65JOFr4BOO7zWlP2tNHAEhA5NBW0z//7B9V5y4MRQnmCArSZMaPXqV+H/PgjI+iKZI8PuTbyMeIp5/D0jSxxpVhIN6KuxN4cbG2yNvVgOUSQJ3T2yJ9VGmAT+wE6UebCiVuYUDcVaWzkDIwm4TRuQrmhAIjfXIe1xPSk3Sy7F5BSLCgSD1GHEX7lc8OfXPoDdDiVOudglCAJUf6qTIp3hkLmjxPz17cydrmcwSYfr5+2jIEktd2Wrgk78HlPN+rY1miMS29umWZRHm032rxypQp2zVLRiPEk0cwdLsRa4rZyail/LYTVlrUoCtbuVwaHddCMGg7/H4eWRAopR9d0+OcgJkZwH9L70ULG0CPyUvkUkaCGANo/9aeOh3U=

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