dolmen

A parser library for automated deduction
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.intf
Module Dolmen_intf . Term . Ae_Arith . Int
include Ae_Arith_Common with type t := t
val minus : t -> t

Arithmetic unary minus/negation.

val add : t -> t -> t

Arithmetic addition.

val sub : t -> t -> t

Arithmetic substraction

val mul : t -> t -> t

Arithmetic multiplication

val pow : t -> t -> t

Arithmetic exponentiation

val lt : t -> t -> t

Arithmetic "less than" comparison.

val le : t -> t -> t

Arithmetic "less or equal" comparison.

val gt : t -> t -> t

Arithmetic "greater than" comparison.

val ge : t -> t -> t

Arithmetic "greater or equal" comparison.

val div_e : t -> t -> t

Euclidian division quotient

val rem_e : t -> t -> t

Euclidian division remainder

val to_real : t -> t

Conversion from an integer term to a real term.