A Coercion from natural numbers into ordinal terms

Consider the following definition of ordinal terms as an inductive type:
Inductive Ord : Set :=
| zero : Ord
| succ : Ord -> Ord
| limit : (nat->Ord)->Ord.

Fixpoint plus (o1 o2:Ord){struct o2} :=
  match o2 with zero => o1
              | succ o2' => succ (o1 + o2')
              | limit f => limit (fun n => plus o1 (f n))
  end.

Notation  "o1 + o2" := (plus o1 o2):o_scope.
Open Scope o_scope.


It is natural to consider the set of natural numbers as a subset of ordinal terms. Formalize it as a coercion from the type nat into Ord. The following code must be accepted by the Coq compiler.
Definition omega := limit (fun n => n).

Check (succ 23).

Check (succ (3+5)).

Eval compute in (succ (3+5)).

Check (omega = 2+omega).

Solution

Look at this file .
Going home