dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Module Dolmen_type . Arith . Tptp . Tff . T . Int
include Dolmen.Intf.Term.Tptp_Tff_Arith_Common with type t := Type.T.t
val minus : Type.T.t -> Type.T.t

Arithmetic unary minus/negation.

val add : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic addition.

val sub : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic substraction

val mul : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic multiplication

val div_e : Type.T.t -> Type.T.t -> Type.T.t

Euclidian division quotient

val div_t : Type.T.t -> Type.T.t -> Type.T.t

Truncation of the rational/real division.

val div_f : Type.T.t -> Type.T.t -> Type.T.t

Floor of the ration/real division.

val rem_e : Type.T.t -> Type.T.t -> Type.T.t

Euclidian division remainder

val rem_t : Type.T.t -> Type.T.t -> Type.T.t

Remainder for the truncation of the rational/real division.

val rem_f : Type.T.t -> Type.T.t -> Type.T.t

Remaidner for the floor of the ration/real division.

val lt : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "less than" comparison.

val le : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "less or equal" comparison.

val gt : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "greater than" comparison.

val ge : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "greater or equal" comparison.

val floor : Type.T.t -> Type.T.t

Floor function.

val ceiling : Type.T.t -> Type.T.t

Ceiling

val truncate : Type.T.t -> Type.T.t

Truncation.

val round : Type.T.t -> Type.T.t

Rounding to the nearest integer.

val is_int : Type.T.t -> Type.T.t

Integer testing

val is_rat : Type.T.t -> Type.T.t

Rationality testing.

val to_int : Type.T.t -> Type.T.t

Convesion to an integer.

val to_rat : Type.T.t -> Type.T.t

Conversion to a rational.

val to_real : Type.T.t -> Type.T.t

Conversion to a real.