a

b

c

d

Type Constructors

List :a ->b

[__] :a ->b

m :(a ->b) ->c

nt :a �(b ->c) �c ->d %(var)%

r :Type

r1 :Type< t

r2 :Type< (t2,r2,s2)

s :Type

s1 :Type< t

s2 :Type< (t2,r2,s2)

s3 :Type< t = {x : t . x = x}

t :Type

t1 :Type< t

t2 :Type< (t2,r2,s2)

tuple1 :b ->a

tuple3 :a �b �c ->d

{__} :a ->b

Assumptions

o1 : m

o2 : (m)(tuple1)

o3 : (m)(tuple3)

o4 : (nt)((r,List,s))

u : ([__])(r)

v : ((m)(List),({__})(s))

x : (tuple3)((r,s,t))

y : (tuple3)((r,s))

z : (m)(([__])(__))

Hint (7,8) not a class '[r]'

Hint (7,15) not a class '{s}'

Hint (11,9) not a class 'tuple3 (r,s,t)'

Error (12,16) incompatible kind of type '(r,s)'

Hint (12,9) not a class 'tuple3 (r,s)'

Error (18,14) undeclared type '__'

Error (18,11) incompatible kind of type '([__])(__)'

Hint (18,9) not a class 'm [__]'

Hint (24,10) not a class 'm'

Error (28,12) incompatible kind of type 'tuple3'

Hint (32,10) not a class 'nt (r,List,s)'

Warning (38,9) unchecked formula 'x = x'