Imandra_prelude.Ordinal
We need to define ordinals before any recursive function is defined, because ordinals are used for termination proofs.
type t =
| Int of int
| Cons of t * int * t
val pp : Stdlib.Format.formatter -> t -> unit
val of_int : int -> t
val (~$) : int -> t
val (<<) : t -> t -> bool
val plus : t -> t -> t
val simple_plus : t -> t -> t
val (+) : t -> t -> t
val of_list : t list -> t
val pair : t -> t -> t
val triple : t -> t -> t -> t
val quad : t -> t -> t -> t -> t
val shift : t -> by:t -> t
val is_valid : t -> bool
val is_valid_rec : t -> bool
val zero : t
val one : t
val omega : t
val omega_omega : t