Module Prelude_extracted.Ordinal

We need to define ordinals before any recursive function is defined, because ordinals are used for termination proofs.

type t =
  1. | Int of int
  2. | Cons of t * int * t
    (*

    cons a x tl is x·(ω^a) + tl, where tl < ω·a, a≠0, x≠0

    *)

Ordinals, up to ε₀, in Cantor Normal Form

val pp : Stdlib.Format.formatter -> t -> unit
val of_int_unsafe : int -> t
val zero : t
val one : t
val two : t
val of_int : int -> t
val (<<) : t -> t -> bool

special axiom: the original well founded relation we use for proving all the other functions terminating.

val plus : t -> t -> t

Addition of ordinals. Not commutative.

val shift : t -> t -> t
val pair : t -> t -> t
val triple : t -> t -> t -> t
val quad : t -> t -> t -> t -> t
val simple_plus : t -> t -> t
val of_list_rec : t -> t list -> t
val of_list : t list -> t
val is_valid_rec : t -> bool

Is this a valid ordinal?

val is_valid : t -> bool

Is this a valid ordinal?

val (+) : t -> t -> t
val (~$) : int -> t
val omega : t
val omega_omega : t