The new interval library

- `x <= y ?< if c` (lersif) has been replaced with `x < y ?<= if c'` (lteif)
  where `c'` is negation of `c`. This change makes statements of several lemmas
  (e.g., `lteif_orb`) easily comprehensible.
- The first constructor `BOpen_if` of `itv_bound` has been replaced with
  `BClose_if` where the first argument is inverted. Now `pred_of_itv` is defined
  by using `lteif` instead of `lersif`.
- Intervals of `T : porderType` form a `porderType` where the ordering relation
  is the subset relation. If `T` is a `latticeType`, intervals also form a
  `latticeType` where the join and meet are intersection and convex hull
  respectively. They are distributive if `T` is an `orderType`.

0 files changed, 0 insertions, 0 deletions