package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.OrdinalSource

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.

Sourcetype t = private
  1. | Zero
  2. | Sum of (int * t) list
Sourceval zero : t
Sourceval const : int -> t
Sourceval mult_const : int -> t -> t
Sourceval of_list : (int * t) list -> t
Sourceval add : t -> t -> t
Sourceval mult : t -> t -> t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval to_string : t -> string
OCaml

Innovation. Community. Security.