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: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 17:09:55 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 10.mo4.mail-out.ovh.net
Autocrypt: addr=mail AT maximedenes.fr; prefer-encrypt=mutual; keydata= xsFNBFRYkvgBEAC0Zot4S5lKkhzYK68sSb69wVyEsugASVeWPHjVpxgFG44BLFB7Te0zWHjg jK76yCUmDdpKFdIufw5PQr+3At/8G75Y3x+dGC2rg+31fPAUJvp/AfrMloH+qd+tqxbaKjtC kymLGE01Yj8m3xaV7bN9wuYwL03+staTESJFVm3CZwNAqFgIZCG6KgBGT93ybUgbPYRrTv+n Oleags7nHdPubX6SAWbZVhuweHCwiooRBVSjzyxuhTtDuAwmeZ+ca4WE3IkOWmJmq4KbCeij HJ9B2b6qSopM19dq+iBByPu+LpBCwSA9Nr9hL1XRnoNngwf0OtJ0CNiKjKsNKlAmsCHw/o48 0IoiKP40sH+zsNFeNepbIqILPaWDvTOFvtHc9FDcH2X9NHaWx73GckMzi2z5Ty4tVoEU4Tap JlDVaKWyhvtHRwxbekgk3Vq3PcKKhcLy/xsbyknVLFw8UbFj+sYwGPrzb7j2WhpisfSct3Ii vxv2FUzM3etqM+tsJ/1Oq8u1A5lQ7lSEZmsCQdeyzMXmrUgXAEZvcx5anmTlNR3TjoG6sOxm axp9f/zgZmr9pV/FRq9tLIu8Eqv8+HqeUcHfxICcnXHVPz2x1h6H6ft45h9LGPEi1riCiZZ5 eFnq/epTkpQF411fo7sY1osaZ0Sp9yrHIPAtmJT40tmPQflSYQARAQABzSZNYXhpbWUgRMOp bsOocyA8bWF4aW1lLmRlbmVzQGlucmlhLmZyPsLBdwQTAQoAIQUCVFiS+AIbAwULCQgHAwUV CgkICwUWAgMBAAIeAQIXgAAKCRAWr2+lkXvTQPz8D/4lUpXfqOp0ZVc9WTBr8bDxHE334Bd9 FnekcYCRrmOUE76oMsK1/MhoKCEmr5bdyn8oh/r2GsNTWB1lsHpTEjYc2Sf17LNW2ncVu4OB EsD38chB9aTEev5Pc2jAA7l/WF8ceF5mkt6OjWrBfDp6yBfXwrzDfdzLixVHVyJUYA/04T7U JZc7Rjz1CdXE2wg8KL7+uq/QGc5TCPPQmlpdXJYpDgK7FtJasRoh34/pVFGHXXA1PnCe+IIL 52DynkF+bCL3sWk8A71ebUkyTO6ytqUKYafCPjrrGv4y13O+/2QcB3Iz4gDiKgvL8FWMhmhJ QF5C8BucOE87JWb5nJmq+Gs13NVofYMpmI+DDaBNJ6ns/sbR68vRfoXEhr0adPDLZOohZKJM Lu6WTjyFNNOgj1jgG0I00+tctmtW00W+U3oi36vbUXalbi5WPlIBpIXkjI9p7xoHe1mJwN40 jn/ExEXnY9uZ4H/NorJ7OzGdEOlz+ZpkcBpW34N5GZfOg7UXScA3tAFPyWcxCKsxAti0sRAR fIQXkxwt+BTBMm5m7n+wxe/2sf+xxO6AYyedWRbLaTCexJEw4Tx4+hocFT8lD6y/cGPORcak AkoWz2aiGQK07gbJ5dxymCP6g0Xcl8CloXodwV124G2++eQpucydK4BRFDTyJLJJNAR3nkei s1BBj87BTQRUWJL4ARAAqLecjPrMCx42r822nQT6e8GTHrFKwppkRqSXAucAZ4ICJ1YoT2Hy z+DtehqEV5IdIDGRivKvQYQF1Yz2NpgO7vfmB1M8ZsxyTyFeQiBkFIb5BKVhUk0xat2Xjgmb PJ59GsEbH5DCIrUqFRRGshjgul/z0adUF5DjFyuqo5TMAJdgXtJbTzmCTXoBwJmNuaUHwieK s47K9pmnnaUnkSy+CDTjtOihNeSx+lmrzieo8OyYuwvY1V1av+dJlF6YF7D5X9gHUAMsSypq pdQX0PhUZ4XheCiC0HojVzT3NEEkZ3LjuAGD7+1yaWNepGgqFqiaGEq4ihjihbvW3rCO84RS 9rSb6F7Eru7HMDUKLmUDc37GhOC0xcrTJ5zZ0CwTaM6V2P2n/FxOXEoKwRVGdAAWvh521N7k pYQpGsamfCzl8ruaEf/IhksPZiyJC95W5jXl98UDf6WNm/xKXwF60oK56iSBj+YWmUgjAzGf XRCJyiXAlMtBhErkije2iIqKVungP3N4IPEhmDOLVa9BsdXAsptkWSmWzvJA+z0A52hta0/2 B71dreoGFVnmLWWSCR+O6P9yivnfEKq75QPjBLj6xw6nXxtyhyrVT2/xOy1Osvf2mM7Gx9wR Q0Ktv7fjX2AyIrcvR3r3/RgsDA3/elqkcrY1hdu+NkOHOKtME43htXsAEQEAAcLBXwQYAQoA CQUCVFiS+AIbDAAKCRAWr2+lkXvTQNfiD/0fD2LeHa/7Vq7ClzMgjaCm5Jt2afGZi9xrD+Z8 4/wlVjFI8TZsYoiq6OTbvn6eNFE7J0wYpAouYS6GP/Ga+e/eo9Hm3BeK9+1gP0QSfwcA1+ci n+zvD5q58Movy7qo4BOoJM2eb8FpdyeloViTUlxgqocZK35ewTK0q3JcMlSZZxdOvCol3F8r CWkXqHlJoA9dL16VxBbxmT57ogqgpOFfIbc9PHMjQaNY5BWLz1+qj4bXN5UXvibP97tas1LE 4OilGPIW/ZOMItfVcxi9//huyTJt0l4lRJRochpmppItYeDs6tFyFu4XpEgUbAXwTnANqHr2 N0OSZT3j+BTMgVrs5sUgjMlqNJkMKjZmkIuSoIZbtYHfQgSY2VBPImLyWpu+XdzjBwFbuMJK 8q9tvgG2ydZCDbpC6Bi0FF+WKmZZqSkqgIFjUOkLGh624JQLbU/aezYrrhORDGEIAGtHbdn3 pC1fcAJHwI3JpRpNwou+lc8SORjUoTpSOmc5C0qWu0P7D1Y3k8gFngN/c42TX6eyyVpQw44h A6bxBs56DrE8OPyt15lveeMxT/0scd/MJlFJY/Dy+XelA0Utt0SUgSqI+TaL2eTlwNCmhNL+ ShCTVRcfb1UFlSA+GyURCLoUjrbukm7GS0pKhF+O9eCj1DkYEdi9NTjs83wKHHYu8CspWw==
Ironport-phdr: 9a23:4CVi+xOwYI16b9PzsxEl6mtUPXoX/o7sNwtQ0KIMzox0Lf7/rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJN/dzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cPOvxXrob8p1sLsxS1GAeiA/npyjhRnX/9wKo30+E7HgHH2AwtBNcOv27brdX0MacdT/26w7fOzTrddPNawzn96JLRfx0nvPqCXqpwfNLMxUQsFA7JlEicpI3lMj+P2OkAvXKX4/d8We+rk2Irtg98rzu1ysooi4TFnJwZxkzY+Slj3Yo4Jtu1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43xqAatZKheSgKz5sqywTaa/OdcoiI5gvvVOGMITdknn5lf6y/hxao/Uim1OL8StG40FdMriVbjtnBrm0B2h/Q58SdV/dw/0es1SyB2g3d8O1IPFw4mK7DJ54k2LEwl54TsUrZHi/xnUX7lKqWeV8l+uis8OnnZ6/pp5CdN49xlA7xL7ohmsqhDuQjKAQOUXKb9fym1LL/5U35XKlKjvoun6bFt5DaPN0XqbK9Aw9IyYku8A2/Djej0NQAh3YLNlNFeBSdj4joIV7COv74De3sy2irxTxs3rXNOqDrKpTLNHnK1rn7Lphn7EsJ7QMjzNVSr77VDDEaaKb2U071nNnRHh48PgC5xev8TttngNBNEVmTC7OUZfuB+WSD4fgidrHVNd0l/Q3lIv1g3MbAyHowmFsTZ66shMVFbXmoH/FrL0ifbGGqjM1TSD5W7Dp7d/TjjRi5aRAWf2y7Bvxu4zgrCYerAYrFS5vrjqbThH7mTK0TXXhPDxW3KVmtd4iAXK1ROnvKZMpmznoBXLmlDog8yVepqg+8zbd7fLLZ
Openpgp: preference=signencrypt

It looks like ultrafinitist parsing :)

Maxime.

On 05/14/2018 04:47 PM, Gaëtan Gilbert wrote:
> Unimath defines a small number of notations in their Preamble.v. Any
> other numbers are not covered.
>
> Notation "0" := (O) : nat_scope.
> Notation "1" := (S 0) : nat_scope.
> Notation "2" := (S 1) : nat_scope.
> Notation "3" := (S 2) : nat_scope.
> Notation "4" := (S 3) : nat_scope.
> Notation "5" := (S 4) : nat_scope.
> Notation "6" := (S 5) : nat_scope.
> Notation "7" := (S 6) : nat_scope.
> Notation "8" := (S 7) : nat_scope.
> Notation "9" := (S 8) : nat_scope.
> Notation "10" := (S 9) : nat_scope.
> Notation "11" := (S 10) : nat_scope.
> Notation "12" := (S 11) : nat_scope.
> Notation "13" := (S 12) : nat_scope.
> Notation "14" := (S 13) : nat_scope.
> Notation "15" := (S 14) : nat_scope.
> Notation "16" := (S 15) : nat_scope.
> Notation "17" := (S 16) : nat_scope.
> Notation "18" := (S 17) : nat_scope.
> Notation "19" := (S 18) : nat_scope.
> Notation "20" := (S 19) : nat_scope.
> Notation "21" := (S 20) : nat_scope.
> Notation "22" := (S 21) : nat_scope.
> Notation "23" := (S 22) : nat_scope.
> Notation "24" := (S 23) : nat_scope.
> Notation "100" := (10 * 10) : nat_scope.
> Notation "1000" := (10 * 100) : nat_scope.
>
>
> Gaëtan Gilbert
>

[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