Legend:
Library
Module
Module type
Parameter
Class
Class type
An ordered type of finite values, extended with positive and negative infinites as well as successor and predecessor functions to represent strict lower and upper bounds.
Negative and positive infinites are used to represent half-planes as intervals; we require that all values are larger than the negative infinite and smaller than the positive infinite.
Values of the form x + \epsilon and x - \epsilon are used to transform open bounds in the finite type into closed bounds on the extended type t, with the equivalence:
y <= x - \epsilon \Leftrightarrow y < x
and
x + \epsilon <= y \Leftrightarrow y < x
This signature does not expose x + \epsilon and x - \epsilon values directly; instead, we use \mathrm{succ} and \mathrm{pred} functions which can be thought of as addition and subtraction of \epsilon, respectively.
Each element of the ordered type t has a successor. The successor of an element is always greater than the element itself:
\forall x, x \le \mathrm{succ}(x)
We say that x is a finite upper bound if it is strictly smaller than its successor, i.e. if x < \mathrm{succ}(x), and we require that all finite values are finite upper bounds (however there may be finite upper bounds that are not finite values).
Each element of the ordered type t has a predecessor. The predecessor of an element is always smaller than the element itself:
\forall x, \mathrm{pred}(x) \le x
We say that x is a finite lower bound if it is strictly greater than its predecessor, i.e. if \mathrm{pred}(x) < x, and we require that all finite values are finite lower bounds (however there may be finite lower bounds that are not finite values).