vars a : Ord; b : BoundedOrd
ops __<=__ : Pred (a * a);
. x <= y /\ y <= z => x <= z
. x <= y /\ y <= x => x = y
type instance a * b : Ord
. (x, v) <= (y, w) <=> x <= y /\ v <= w;
class instance DiscreteOrd < Ord
vars a : DiscreteOrd; x, y : a
op __<=__ : Pred ((a ->? b) * (a ->? b))
type instance a ->? b : Ord
. x <= y <=> def x () => x () <= y ();
%% Classes ---------------------------------------------------------------
%% Type Variables --------------------------------------------------------
%% Assumptions -----------------------------------------------------------
__<=__ : forall a : Ord . Pred (a * a) %(op)%
bot : forall b : BoundedOrd . b %(op)%
min : forall b : Num . b * b ->? b %(op)%
top : forall b : BoundedOrd . b %(op)%
%% Variables -------------------------------------------------------------
%% Sentences -------------------------------------------------------------
x <= y /\ y <= z => x <= z
x <= y /\ y <= x => x = y
(x, v) <= (y, w) <=> x <= y /\ v <= w
x <= y <=> def x () => x () <= y ()
%% 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 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'
### 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'
### 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)'
is not unifiable with type 'Unit ->? ? _v195'
### Hint, in type of '(var x : ? a)'
is not unifiable with type 'Unit ->? _v203' (41.25)
### Hint, in type of '(var y : ? a)'
is not unifiable with type 'Unit ->? _v204' (41.32)