-------------------------------- MODULE Reals ------------------------------- (***************************************************************************) (* This module provides dummy definitions of the operators that are *) (* defined by the real Reals module. It is expected that any tool that *) (* handles specifications that use real numbers will provide its own *) (* implementations of these operators. TLC currently does not handle real *) (* numbers and produces an error if a specification requires TLC to *) (* evaluate the operators defined here or to evaluate any operator defined *) (* in the Integers module that is applied to non-integer real numbers. *) (* *) (* See the book "Specifying Systems" for the real Reals module. *) (***************************************************************************) EXTENDS Integers Real == "Reals" a / b == CHOOSE m \in Real : m * b = a Infinity == CHOOSE i : (i \notin Real) /\ (\A r \in Real : i > r) =============================================================================