package smtml

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

Module Make.RealSource

Sourceval neg : term -> term

neg t constructs the negation of the real number term t.

Sourceval to_int : term -> term

to_int t converts the real number term t to an integer term.

Sourceval add : term -> term -> term

add t1 t2 constructs the sum of the real number terms t1 and t2.

Sourceval sub : term -> term -> term

sub t1 t2 constructs the difference of the real number terms t1 and t2.

Sourceval mul : term -> term -> term

mul t1 t2 constructs the product of the real number terms t1 and t2.

Sourceval div : term -> term -> term

div t1 t2 constructs the quotient of the real number terms t1 and t2.

Sourceval pow : term -> term -> term

pow t1 t2 constructs the power of the real number terms t1 and t2.

Sourceval lt : term -> term -> term

lt t1 t2 constructs the less-than relation between t1 and t2.

Sourceval le : term -> term -> term

le t1 t2 constructs the less-than-or-equal relation between t1 and t2.

Sourceval gt : term -> term -> term

gt t1 t2 constructs the greater-than relation between t1 and t2.

Sourceval ge : term -> term -> term

ge t1 t2 constructs the greater-than-or-equal relation between t1 and t2.