Ordre total

VIRTUAL TYPE total_order {t: type}
  INHERIT partial_order{t} HIDE "~<" "~>" "~<=" "~>="
    -- These operations are redundant for a total order,
    -- use >=, <=, >, and < instead.
  EXPORT Exhaustive Total_ordering

  MESSAGE "<="(x y: t) REPLY(b: boolean)
    WHERE Exhaustive("<=")

  MESSAGE max(x y: t) REPLY(z: t)
    WHERE z = IF x >= y THEN x ELSE y FI

  MESSAGE min(x y: t) REPLY(z: t)
    WHERE z = IF x <= y THEN x ELSE y FI

  CONCEPT Exhaustive(f: function{t, t, boolean})
    VALUE(b: boolean)
      WHERE b <=> ALL(x y: t :: f(x, y) | f(y, x))

  CONCEPT Total_ordering(f: function{t, t, boolean})
    VALUE(b: boolean)
      WHERE b <=> Partial_ordering(f) & Exhaustive(f)
END