Make.Real
val neg : term -> term
neg t constructs the negation of the real number term t.
neg t
t
val to_int : term -> term
to_int t converts the real number term t to an integer term.
to_int t
val add : term -> term -> term
add t1 t2 constructs the sum of the real number terms t1 and t2.
add t1 t2
t1
t2
val sub : term -> term -> term
sub t1 t2 constructs the difference of the real number terms t1 and t2.
sub t1 t2
val mul : term -> term -> term
mul t1 t2 constructs the product of the real number terms t1 and t2.
mul t1 t2
val div : term -> term -> term
div t1 t2 constructs the quotient of the real number terms t1 and t2.
div t1 t2
val pow : term -> term -> term
pow t1 t2 constructs the power of the real number terms t1 and t2.
pow t1 t2
val lt : term -> term -> term
lt t1 t2 constructs the less-than relation between t1 and t2.
lt t1 t2
val le : term -> term -> term
le t1 t2 constructs the less-than-or-equal relation between t1 and t2.
le t1 t2
val gt : term -> term -> term
gt t1 t2 constructs the greater-than relation between t1 and t2.
gt t1 t2
val ge : term -> term -> term
ge t1 t2 constructs the greater-than-or-equal relation between t1 and t2.
ge t1 t2