The Coq mailing list

[nikhil kaushik <nikhilka585 AT gmail.com>]

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