package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Syntactic Ordinals

Ordinals as defined in "Transfinite KBO", up to ε₀. Some basic operations are defined.

An ordinal is either 0 or a finite sum Σ_i nᵢ . ω^bᵢ where each bᵢ is itself an ordinal.

NOTE: experimental module; also performance might not be great.

type t = private
  1. | Zero
  2. | 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 to_string : t -> string