class Cpo

var a : -Cpo

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

type Nat

ops 1 : Nat;

__+__ : Nat * Nat -> Nat

type Chain a =

{s : Nat ->? a . forall n : Nat . def s n => s n <= s (n + 1)}

var a : Cpo

fun sup : Chain a ->? a

vars x : ? a; c : Chain a

. sup c <= x <=> forall n : Nat . c n <= x;

types

Chain : Cpo -> Type;

Nat : Type;

gn_t5[Chain] : -Type -> +Type -> Type

type

gn_t5[Chain] < __->?__

type

Chain := gn_t5[Chain] Nat

var

a : Cpo %(var_6)%

op 1 : Nat

op __+__ : Nat * Nat -> Nat

fun __<=__ : forall a : -Cpo . Pred (a * a)

fun sup : forall a : Cpo . Chain a ->? a

vars

c : Chain a;

x : ? a

forall a : -Cpo

. forall s : Nat ->? a

. (s in Chain a) <=> forall n : Nat . def s n => s n <= s (n + 1)

forall a : Cpo; c : Chain a; x : ? a

. sup c <= x <=> forall n : Nat . c n <= x

1.7-1.9: ### Warning: unchanged class 'Cpo'

2.8: ### Hint: is type variable 'a'

3.25: ### Hint:

no kind found for 'a'

expected: {Cppo}

found: {Cpo}

5.27-5.29: ### Hint:

no kind found for 'Nat'

expected: {Cpo}

found: {Type}

5.27-5.29: ### Hint:

no kind found for 'Nat'

expected: {Cppo}

found: {Type}

6.15: ### Hint: rebound type variable 'a'

7.35: ### Hint: not a class 'Nat'

8.8: ### Hint: is type variable 'a'

8.8: ### Hint: rebound type variable 'a'

10.9: ### Hint: not a kind '? a'

10.16: ### Hint: not a kind 'Chain a'

11.26: ### Hint: not a class 'Nat'