BoundedOrd.hascasl revision 4ea69d9a971bbb8b4082bcd60350fdabd5411c23
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: Ord; x: a
1a6464613c59e35072b90ca296ae402cbe956144Christian Maederop __<=__ : Pred (a * a)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederclasses BoundedOrd < Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: Ord; b: BoundedOrd
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop __<=__ : Pred (a * a);
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars x, y, z: a; v: b
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. x <= y /\ y <= z => x <= z
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. x <= y /\ y <= x => x = y
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a, b: +Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype instances a * b: Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars x, y: a; v, w: b
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder. (x, v) <= (y, w) <=> x <= y /\ v <= w
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederclass instance DiscreteOrd < Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: DiscreteOrd; x, y: a
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. x <= y <=> x = y
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: Ord; b: Num
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederops min: a * a ->? a;
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder min: b * b ->? b
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: Ord; b: Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop __<=__ : Pred ((a ->? b) * (a ->? b))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedervars a: -Ord; b: +Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype instance a ->? b: Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype instance Unit: Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype instance ?a: Ord
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. x <= y <=> def x() => x() <= y()