a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzclass Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz {vars a : Ord; x : a

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner op __<=__ : Pred (a * a)

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz . x <= x;

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz }

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzclass BoundedOrd < Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars a : Ord; b : BoundedOrd

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzops __<=__ : Pred (a * a);

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz bot, top : b

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars x, y, z : a; v : b

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. x <= x

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. x <= y /\ y <= z => x <= z

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. x <= y /\ y <= x => x = y

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. bot <= v

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. v <= top;

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars a, b : Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulztype instance a * b : Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars x, y : a; v, w : b

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. (x, v) <= (y, w) <=> x <= y /\ v <= w;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederclass instance DiscreteOrd < Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars a : DiscreteOrd; x, y : a

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. x <= y <=> x = y;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederclass Num

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars a : Ord; b : Num

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzop min : a * a ->? a

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars a : Ord; b : Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzop __<=__ : Pred ((a ->? b) * (a ->? b))

67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulztype instance a ->? b : Ord

67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulztype instance Unit : Ord

dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz. () <= ();

67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulztype instance ? a : Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzvars x, y : ? a

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz. x <= y <=> def x () => x () <= y ();

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzclass Cpo < Ord

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzvar a : Cpo

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzop __<=__ : Pred (a * a)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzvar x : ? a

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz. x <=[? a] x;

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Classes ---------------------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzBoundedOrd < Ord

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzCpo < Ord

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzDiscreteOrd < Ord

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzNum < Type

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzOrd < Type

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Type Constructors -----------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz? : +Ord -> Ord

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz__*__ : +Ord -> +Ord -> Ord

7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz__->?__ : -Ord -> +Ord -> Ord

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Type Variables --------------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulza : Cpo %(var_197)%

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzb : Ord %(var_157)%

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz%% Assumptions -----------------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz__<=__ : forall a : Ord . Pred (a * a) %(op)%

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzbot : forall b : BoundedOrd . b %(op)%

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzmin : forall a : Ord . a * a ->? a %(op)%

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztop : forall b : BoundedOrd . b %(op)%

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Variables -------------------------------------------------------------

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzv : b

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzw : b

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzx : ? a

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzy : ? a

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzz : a

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Sentences -------------------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= x

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= x

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= y /\ y <= z => x <= z

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= y /\ y <= x => x = y

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzbot <= v

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzv <= top

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz(x, v) <= (y, w) <=> x <= y /\ v <= w

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= y <=> x = y

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz() <= ()

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= y <=> def x () => x () <= y ()

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzx <= x

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz%% Diagnostics -----------------------------------------------------------

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 2.7, is type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 2.16, not a class 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 8.7, is type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 8.7, rebound type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 8.15, is type variable 'b'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 9.16-9.22, repeated declaration of '__<=__' with type 'Pred (a * a)'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 11.8, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 11.7, rebound variable 'x'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 11.11, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 11.14, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 11.20, not a class 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 18.7, is type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 18.7, rebound type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 18.10, is type variable 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 18.10, rebound type variable 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.8, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.7, rebound variable 'x'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.11, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.10, rebound variable 'y'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.17, not a class 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.16, rebound variable 'v'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 20.20, not a class 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.7, is type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.7, rebound type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.24, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.23, rebound variable 'x'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.27, not a class 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 24.26, rebound variable 'y'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 28.7, is type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 28.7, rebound type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 28.15, is type variable 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 28.15, rebound type variable 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 30.12-30.22, no kind found for 'b'

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz expected: {Ord}

a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz found: {Num}

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz*** Error 30.7, equal type schemes with uncomparable constraints of 'min'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 30.12-30.18, uncomparable declaration of 'min' with type 'b * b ->? b'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 32.7, is type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 32.7, rebound type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 32.15, is type variable 'b'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 32.15, rebound type variable 'b'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 33.16-33.43, no kind found for 'a ->? b'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz expected: {Ord}

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz found: {Type}

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Warning 33.9, overlapping declaration of '__<=__'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 40.8, not a kind '? a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 40.7, rebound variable 'x'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 40.11, not a kind '? a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 40.10, rebound variable 'y'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 41.18, in type of '(var x : ? a)'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz typename 'a' (40.14)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz is not unifiable with type 'Unit ->? ? _v187_a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 41.25, in type of '(var x : ? a)'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz typename 'a' (40.14)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz is not unifiable with type 'Unit ->? _v195' (41.25)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 41.32, in type of '(var y : ? a)'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz typename 'a' (40.14)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz is not unifiable with type 'Unit ->? _v196' (41.32)

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 44.5, is type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 44.5, rebound type variable 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 45.16-45.27, no kind found for 'a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz expected: {Ord}

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz found: {Type}

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 45.16-45.22, ignored specialized declaration of '__<=__' with type 'Pred (a * a)'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 47.6, not a kind '? a'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 47.5, rebound variable 'x'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz### Hint 48.7-48.10, is type list '[? a]'

6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz