Что такое конструктор в Coq?

Мне сложно понять принципы того, что такое конструктор и как он работает.

Например, в Coq нас учили определять натуральные числа следующим образом:

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

И нам сказали, что S является конструктором, но что именно это означает?

Если я тогда do:

Check (S (S (S (S O)))).

Я понимаю, что это 4 и тип nat .

Как это работает, и откуда Coq узнает, что (S (S (S (SO)))) представляет 4 ?

Думаю, ответ на этот вопрос - очень умная магия фона в Coq .