Real.Interval
Intervals over the value
type.
type bnd = bnd
The type of the interval bounds.
type t = bnd Intervals_intf.interval
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
.
val pp : t Fmt.t
Pretty-printer for intervals.
val of_bounds : value Intervals_intf.bound -> value Intervals_intf.bound -> t
Build an interval from a pair of lower and upper bounds.
val view : t -> value Intervals_intf.bound Intervals_intf.interval
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)
.
val full : t
The full interval [-\infty, +\infty]
contains all values.
This is an equivalent shortcut for of_bounds Unbounded Unbounded
.