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: David P Á <david AT picon.email>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 10:44:06 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david AT picon.email; spf=Pass smtp.mailfrom=david AT picon.email; spf=None smtp.helo=postmaster AT ns3014420.ip-178-32-223.eu
Ironport-phdr: 9a23:JzzBth9NjubJLv9uRHKM819IXTAuvvDOBiVQ1KB40+McTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LWbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUBFeUBI+dYoJTlqFUUtRS7ARSnCeTyxTBSmH/23LA13v85EQHHwAMgGNQOvG7Ko9XwLqgSUOS1wbDOwD7ebP1WwS/w5JXKfx0iu/2BU6x8fdDPxUUxGQ7JlFadpI79Mz6W2OkBqXWX4utgWO61lmIrtw58riKxysswiITEgJ8exEre+iVj2ok1IMW1SE5lbt6gF5tdryeaN5B4T88+Xm1ltyk3xqMatZKhfSgK0I0rywPdZvGEaoSF7AzvWP+PLTtmin9pYqywhwuq/UihzO3zSNW03U5XoidHkdTArH4A2wLJ5sSZVPdw8F2t1DWN2gzL7+FLO0E0la7VK547xb4wk4IevlnZES/omUX5kbSbdl0l+ue07OTnZK/qqYGZN4BuiwH+NrwimtajDuQgLggOQ2+b9Pyg273k5E31WalFjvkrkqbCq53aPsQapquhAwBPyIoj6hC/Dy2n0NsCh3UHIkhFK1q7iN3iPEiLK/TlB9++hU6tmXFl3aPoJLrkV7nEMHnPp4/W1P4p50dCyQYb1dFU4JQSB7QIIfalCRy5j8DREhJsa1/8+O3gEtgojtpPC1LKObeQNebpiXHN4+suJ+eWY4pM42TlKvMi4bjjiHY4nQ1EJPX77d4scHm9W89eDQCBe3O12YUZEGwNuEwzSeXrjA/aCGMBVzOJR6s5owoDJsemAIPEHND/hqfahH7nQscOIGFeTwnTQTKzLcDeAaxKZT/AesI=

On 14/05/2018 10:34, Gergely Buday wrote:

How does Coq relate the above user definition to the standard way of
writing natural numbers?

It's Coq syntactic sugar, as Software Foundations points out eventually. It would otherwise become far too tedious to represent naturals.

--David.

[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