null
Constrain.hascasl.output revision 6cb518d88084543c13aa7e56db767c14ee97ab77
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
class Eq
class Ord < Eq
type a : Ord
op f : forall e : Ord . e -> e
op c : a
. f (f c) = c;
type t : Eq
op b : t
. f b = b;
classes
Eq < Type;
Ord < Eq
types
a : Ord;
t : Eq
op b : t %(op)%
op c : a %(op)%
op f : forall e : Ord . e -> e %(op)%
. f (f c) = c
. f b = b
### Hint 16.3, constrain 't : Ord' is unprovable
known kinds are: {Eq}
*** Error 16.3, in term '(op f : forall e : Ord . e -> e)[t] (op b : t) = (op b : t)' of type 'Unit'
unresolved constraints '{t : Ord}'