Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Li-yao Xia <lysxia 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 06:24:54 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f54.google.com
  • Ironport-phdr: 9a23:DTF+9hw+AVbmmcLXCy+O+j09IxM/srCxBDY+r6Qd1eMfIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH1likHOT43/mLZhMN+g61Uog6uqRNkzo7IY4yYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YBCesBMf9YrobnoFsFsBqxBQi2C+jyzTJIgn/33bY10uQgCw7LxwMgH9cUv3TVqNX5LrsdUeewzKTRyzjIcvBY2S/l5YTWbhwspeuAULFwfMbL10UjCg3Igk+QpIHqJz+ZyPgBvmmB4+Z9S+6ii3QrpgBvrjS12Mshio/EjZ8PxF/e7yV22oM1KMW4SEFlZd6kF4NdtySAOIt3RsMuWn9ouCUmxrEft562fCcHxI4oxx7YbPyHfIyI7Qz5WOmNJjd4gWppeLO5hxms7Uit0vPwWtWw3VpQrSdIksPAum4Q2xHd8MSKSvRw8l+k2TmV1gDT7u9EIVozlareM5Mhxr4xloEcsETCBCD7g0r2jKqMeUUl/uik8fjoYrLjppOELY97lhn+Mrgymsy4Gek3Lg8OX3GC9eug0L3j4Fb2Ta5Rjvw2l6nZqIrVKd4apq6/GQ9V05ws5wyxDze8g5wkmiwMK0sAcxaahaDoPUvPKbb2F6SRmVOpxRNqguHPOfXRA5yFenzSi6fgdJ5y7kddzEw4ytUJtMEcMa0IPP+mAhy5j9ffFBJsa1XlkdaiM81008YlYUzKB6aYNK3ItlrRv7AgJuCNYMkevzOvcqF5tc6rtmcwnBomRYfsxYEeMSnqEfFvIkHfan3p0I9YTDU6+zEmRemvs2WsFD5eY3HoAvA57zA/TZylVcLNG9zrj7uG0yO2WJZRYzIeBw==
In Basics.v, the new `nat` is defined in a module `NatPlayground`, which is quickly closed, putting the definition out of scope. If you try `Check (S O).` before the `End NatPlayground.` command, so that it uses the user-defined nat, it will not be pretty printed.

Li-yao

On 05/14/2018 05:30 AM, Gergely Buday wrote:
Yes this is obvious and other theorem provers do the same.

The question is: what is the machinery behind this? Does the system
recognizes that this definition is indeed a definition for the natural
numbers?

On 14 May 2018 at 10:44, David P Á <david AT picon.email> wrote:
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.


Archive powered by MHonArc 2.6.18.

Top of Page