The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

This is Coq's way of representing elements of a type. S is the the constructor to add elements to type nat. The letter O represents an element of type (nat), which is normally interpreted as 0 (you can interpret it as another number too) and the constructor S defines a way how to generate other elements starting from the first element O. The constructor S means: if n is a natural then so is S n. Normally, as S is interpreted as the successor of n, so n is the predecessor of S n.  

On Wed, May 24, 2017 at 9:50 AM, nikhil kaushik <nikhilka585 AT gmail.com> 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.

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 preddefinition how does O represent 0? And how does S n' pattern match gives us predecessor of n.

--

~Nikhil Kaushik