coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gergely Buday <gbuday AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] natural numbers as a datatype and as decimal numerals
Date: Mon, 14 May 2018 10:34:01 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gbuday AT gmail.com; spf=Pass smtp.mailfrom=gbuday AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f45.google.com
Ironport-phdr: 9a23:B9rQ1x2DnfM8qC2BsmDT+DRfVm0co7zxezQtwd8ZsewRKvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l75brA67qhBj34LYfIOYOfxjda3dZ9MaQm9BU95QWSNfGIO8YJUAD+4BPO1FsoT9ukYBogG+BAKxA+7vxSRHhmLr0qIg0+UsCg7G3Ak6ENIPtHTYtsn6NKAXUe2syqTD0DbNb+tO1Dvj9ITFdgotrPKMUL5qb8bd1EciGxnKg1iQr4HuIimb2f4Xs2eB6uptTeKvhHAjqwF2ujWvw90jiojNho4M1FDE9jl1zJ87JdC3SEN3e9GkEJxXtyGVM4t5XNkuTH1vuCY/0rEGuJi7czYWyJk/2RLTd/iKf5KL7x/jTuqdPyp0iXx/dL+whxu+6U2gxff9Vsmw3lZKtC1FktzUu3ACzBPT99WIReF9/0q61jaP0hrc6uBAIUwuiaXbLJshzqYqlpUPqUTDAjP2mELugaCKcUUk4/Gk5PjjYrX7vZCRLJR0iwH7MqQ2gMOzG+U4Mg4UX2ia4+uwzrPj/VeqCIlN2/Yxi+zStI3QDcUdvK+wRQFPgag57BPqIDq839kcjDEtMV5MaVrTgIL0N1jfCP/9BPa7xV+rlWE4lLj9IrT9D8CVfTD4m7D7cOMlsh8O+E8I1dlaoqlsJPQEKfP3VFX2sYWBXBA8Og2whe3gDYckj99MaSe0GqacdZjqnxqQ/Ot2eruDYYYUvHD2LP13v6ez3098okcUeOyS5bVSaH28Ga47cUCQYH6pnNRZVGlW40wxS+vljFDEWjlWNS6/

Hi,

in Software Foundations' first file, Basics.v, the file defines

Inductive nat : Type :=
| O : nat
| S : nat -> nat.

and then, magically, uses decimal numerals, 3, 5 and so on for it.

How does Coq relate the above user definition to the standard way of
writing natural numbers? I haven't seen any special declaration in the
file that tells the system to do so.

- Gergely

[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