The Coq mailing list

[Matej Košík <matej.kosik AT inria.fr>]

Hi,

On 05/24/2017 06:50 AM, nikhil kaushik wrote:
> I was going through the book /Software foundations/ to learn /Coq/ and I 
> got stuck on Numbers. In this Type definition
> 
> |Inductive nat : Type := | O : nat | S : nat -> nat. |
> 
> How does |O| becomes |0| when we use it in definition of
> 
> |Definition pred (n : nat) : nat := match n with | O => O | S n' => n' end. 
> |

The fact that 0 means the same thing as O
              1 means the same thing as S O
              2 means the same thing as S (S O)
              3 means the same thing as S (S (S O))
              ...
does not follow from the above definition.

This "syntactic sugar" is provided by the "nat_syntax_plugin" which is one of 
the Coq "plugins" that is loaded by default.

If it is not explained in the Software Foundation (I am not sure whether 
that's the case), then it is an omission in the book.

> 
> I only understood that |O| represents natural numbers and |S| takes a 
> natural number and return another natural number so S is a function. What I 
> do not get is when our defined |nat| data type is used
> in |pred|definition how does |O| represent |0|? And how does |S n'| pattern 
> match gives us predecessor of |n|.
> 
> 
> -- 
> ~Nikhil Kaushik