package alt-ergo-lib

The type of values in the interval.

The type of the interval bounds.

The type of closed intervals with bounds of type bound.

Note that the values of the interval may have a different type; for instance, -\infty and +\infty are valid bounds for real intervals, but are not themselves reals.

We say that an extended value x is a valid lower bound if it satisfies:

        \forall y, y < x \Rightarrow \mathrm{pred}(x) < x
      

Similarly, we say that an extended value x is a valid upper bound if it satisfies:

        \forall y, x < y \Rightarrow x < \mathrm{succ}(x)
      

Remark that valid lower bounds are either -\infty or finite lower bounds, and valid upper bounds are either +\infty or finite upper bounds.

We require that an interval { lb ; ub } be such that lb is a valid lower bound, ub is a valid upper bound, and lb <= ub.

Pretty-printer for intervals.

Equality test for intervals.

Build an interval from a pair of lower and upper bounds.

• raises Invalid_argument

  if the upper bound is smaller than the lower bound.

Returns a view of the interval using the bound type for convenient examination.

The interval singleton v contains the singleton \{ v \}.

This is an equivalent shortcut for of_bounds (Closed v) (Closed v).

The full interval [-\infty, +\infty] contains all values.

This is an equivalent shortcut for of_bounds Unbounded Unbounded.

If the interval is a singleton containing a single value, returns that value; otherwise, returns None.