-------------------------------- MODULE Reals -------------------------------
EXTENDS Integers
LOCAL R == INSTANCE ProtoReals
Real == R!Real
a / b == R!/(a, b)
Infinity == R!Infinity
=============================================================================