Nombres

VIRTUAL TYPE number{t: type}
  INHERIT equality{t}
  EXPORT Commutative Associative Distributive Identity

  MESSAGE zero REPLY(n: t)
    WHERE Identity(zero, "+")

  MESSAGE one REPLY(n: t)
    WHERE Identity(one, "*")

  MESSAGE "+"(n1 n2: t) REPLY(n3: t)
    WHERE Commutative("+"), Associative("+")

  MESSAGE "*"(n1 n2: t) REPLY(n3: t)
    WHERE ALL(n: t :: n * zero = zero),
      Commutative("*"), Associative("*"),
      Distributive("*", "+")

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

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

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

  CONCEPT Identity(i: t, f: function{t, t, t})
    VALUE(b: boolean)
    WHERE b <=> ALL(x: t :: f(x, i) = x = f(i, x))
END