class Ord

{vars a : Ord; x : a

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

. x <= x;

}

class BoundedOrd < Ord

vars a : Ord; b : BoundedOrd

ops __<=__ : Pred (a * a);

bot, top : b

vars x, y, z : a; v : b

. x <= x

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

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

. bot <= v

. v <= top;

vars a, b : Ord

type instance a * b : Ord

vars x, y : a; v, w : b

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

class instance DiscreteOrd < Ord

vars a : DiscreteOrd; x, y : a

. x <= y <=> x = y;

class Num

vars a : Ord; b : Num

op min : a * a ->? a

vars a : Ord; b : Ord

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

type instance a ->? b : Ord

type instance Unit : Ord

. () <= ();

type instance ? a : Ord

vars x, y : ? a

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

class Cpo < Ord

var a : Cpo

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

var x : ? a

. x <=[? a] x;

%% Classes ---------------------------------------------------------------

BoundedOrd < Ord

Cpo < Ord

DiscreteOrd < Ord

Num < Type

Ord < Type

%% Type Constructors -----------------------------------------------------

? : +Ord -> Ord

__*__ : +Ord -> +Ord -> Ord

__->?__ : -Ord -> +Ord -> Ord

%% Type Variables --------------------------------------------------------

a : Cpo %(var_205)%

b : Ord %(var_165)%

%% Assumptions -----------------------------------------------------------

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

bot : forall b : BoundedOrd . b %(op)%

min : forall a : Ord . a * a ->? a %(op)%

top : forall b : BoundedOrd . b %(op)%

%% Variables -------------------------------------------------------------

v : b

w : b

x : ? a

y : ? a

z : a

%% Sentences -------------------------------------------------------------

x <= x

x <= x

x <= y /\ y <= z => x <= z

x <= y /\ y <= x => x = y

bot <= v

v <= top

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

x <= y <=> x = y

() <= ()

x <= y <=> def x () => x () <= y ()

x <= x

%% Diagnostics -----------------------------------------------------------

### Hint 2.7, is type variable 'a'

### Hint 2.16, not a class 'a'

### Hint 8.7, is type variable 'a'

### Hint 8.7, rebound type variable 'a'

### Hint 8.15, is type variable 'b'

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

### Hint 11.8, not a class 'a'

### Hint 11.7, rebound variable 'x'

### Hint 11.11, not a class 'a'

### Hint 11.14, not a class 'a'

### Hint 11.20, not a class 'b'

### Hint 18.7, is type variable 'a'

### Hint 18.7, rebound type variable 'a'

### Hint 18.10, is type variable 'b'

### Hint 18.10, rebound type variable 'b'

### Hint 20.8, not a class 'a'

### Hint 20.7, rebound variable 'x'

### Hint 20.11, not a class 'a'

### Hint 20.10, rebound variable 'y'

### Hint 20.17, not a class 'b'

### Hint 20.16, rebound variable 'v'

### Hint 20.20, not a class 'b'

### Hint 24.7, is type variable 'a'

### Hint 24.7, rebound type variable 'a'

### Hint 24.24, not a class 'a'

### Hint 24.23, rebound variable 'x'

### Hint 24.27, not a class 'a'

### Hint 24.26, rebound variable 'y'

### Hint 28.7, is type variable 'a'

### Hint 28.7, rebound type variable 'a'

### Hint 28.15, is type variable 'b'

### Hint 28.15, rebound type variable 'b'

### Hint 30.12-30.22, no kind found for 'b'

expected: {Ord}

found: {Num}

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

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

### Hint 32.7, is type variable 'a'

### Hint 32.7, rebound type variable 'a'

### Hint 32.15, is type variable 'b'

### Hint 32.15, rebound type variable 'b'

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

expected: {Ord}

found: {Type}

### Warning 33.9, overlapping declaration of '__<=__'

### Hint 40.8, not a kind '? a'

### Hint 40.7, rebound variable 'x'

### Hint 40.11, not a kind '? a'

### Hint 40.10, rebound variable 'y'

### Hint, in type of '(var x : ? a)'

typename 'a' (40.14)

is not unifiable with type 'Unit ->? ? _v195_a'

### Hint, in type of '(var x : ? a)'

typename 'a' (40.14)

is not unifiable with type 'Unit ->? _v203' (41.25)

### Hint, in type of '(var y : ? a)'

typename 'a' (40.14)

is not unifiable with type 'Unit ->? _v204' (41.32)

### Hint 44.5, is type variable 'a'

### Hint 44.5, rebound type variable 'a'

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

expected: {Ord}

found: {Type}

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

### Hint 47.6, not a kind '? a'

### Hint 47.5, rebound variable 'x'

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