Ordre partiel

VIRTUAL TYPE partial_order{t: type}
  INHERIT equality{t}
  EXPORT Acyclic Antisymmetric Partial_ordering

  MESSAGE "<"(x y: t) REPLY(b: boolean)
    WHERE b <=> (x <= y & x ~= y), Acyclic("<"), Transitive("<")

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

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

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

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

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

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

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

  CONCEPT Acyclic(f: function{t, t, boolean})
    VALUE(b: boolean)
    WHERE b <=> ALL(x: t :: ~f(x, x))

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

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