Module Logtk.Ordinal

Syntactic Ordinals

type t = private
| Zero
| Sum of (int * t) list
val zero : t
val const : int -> t
val mult_const : int -> t -> t
val of_list : (int * t) list -> t
val add : t -> t -> t
val mult : t -> t -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val pp : t CCFormat.printer
val to_string : t -> string