BoundedOrd.hascasl revision 2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a: Ord; x: a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederop __<=__ : Pred (a * a)
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederclasses BoundedOrd < Ord
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a: Ord; b: BoundedOrd
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederop __<=__ : Pred (a * a);
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars x, y, z: a; v: b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y /\ y <= z => x <= z
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y /\ y <= x => x = y
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a, b: +Ord
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedertype instances a * b: Ord
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars x, y: a; v, w: b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. (x, v) <= (y, w) <=> x <= y /\ v <= w
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederclass instance DiscreteOrd < Ord
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a: DiscreteOrd; x, y: a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y <=> x = y