vars a, b : Type

generated type Set a ::= empty | add a (Set a)

generated type Sys b ::= node b (Set (Sys b))

type Nat

var a : Type

generated type CTree a ::= leaf a | branch (Nat ->? CTree a)

free type L ::= abs (L -> L)

free type Tree a b ::= leaf b | branch (a -> Tree a b)

free type List a ::= nil | cons (a; List a)

free type Tree a b ::= leaf a | branch (b -> List (Tree a b))

var c : Type

op fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

vars f : a -> c; g : (b -> List c) -> c; x : a;

s : b -> List (Tree a b)

. fold f g (leaf x) = f x

. def fold f g (branch s);

types

CTree : Type -> Type;

L : Type;

List : Type -> Type;

Nat : Type;

Set : Type -> Type;

Sys : Type -> Type;

Tree : Type -> Type -> Type

vars

a : Type %(var_5)%;

b : Type %(var_2)%;

c : Type %(var_12)%

op abs : (L -> L) -> L %(constructor)%

op add : forall a : Type . a -> Set a -> Set a %(constructor)%

op branch : forall a : Type . (Nat ->? CTree a) -> CTree a

%(constructor)%

op branch : forall a : Type; b : Type

. (b -> List (Tree a b)) -> Tree a b

%(constructor)%

op branch : forall a : Type; b : Type . (a -> Tree a b) -> Tree a b

%(constructor)%

op cons : forall a : Type . a * List a -> List a %(constructor)%

op empty : forall a : Type . Set a %(constructor)%

op fold : forall b : Type; a : Type; c : Type

. (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

%(op)%

op leaf : forall a : Type . a -> CTree a %(constructor)%

op leaf : forall a : Type; b : Type . b -> Tree a b %(constructor)%

op leaf : forall a : Type; b : Type . a -> Tree a b %(constructor)%

op nil : forall a : Type . List a %(constructor)%

op node : forall b : Type . b -> Set (Sys b) -> Sys b

%(constructor)%

vars

f : a -> c;

g : (b -> List c) -> c;

s : b -> List (Tree a b);

x : a

generated type Set(a : Type) ::= add (a) (Set a) | empty %(ga_Set)%

generated type Sys(b : Type) ::= node (b) (Set (Sys b)) %(ga_Sys)%

generated type CTree(a : Type) ::=

branch (Nat ->? CTree a) | leaf (a) %(ga_CTree)%

free type L ::= abs (L -> L) %(ga_L)%

free type Tree(a : Type)(b : Type) ::=

branch (a -> Tree a b) | leaf (b) %(ga_Tree)%

free type List(a : Type) ::= cons (a; List a) | nil %(ga_List)%

free type Tree(a : Type)(b : Type) ::=

branch (b -> List (Tree a b)) | leaf (a) %(ga_Tree)%

forall

a : Type; b : Type; c : Type; f : a -> c; g : (b -> List c) -> c;

x : a

. fold f g (leaf x) = f x

forall

a : Type; b : Type; c : Type; f : a -> c; g : (b -> List c) -> c;

s : b -> List (Tree a b)

. def fold f g (branch s)

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

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

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

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

### Hint 15.11, redeclared type 'Tree'

### Hint 17.5, is type variable 'c'

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

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

### Hint 20.20, not a kind '(b -> List c) -> c'

### Hint 20.44, not a class 'a'

### Hint 20.51, not a kind 'b -> List (Tree a b)'

### Hint 21.13,

in type of '(op leaf : forall a : Type . a -> CTree a)'

typename 'CTree' (7.16)

is not unifiable with type 'Tree a' (20.10)

### Hint 21.18, rejected 'a < b' of '(var x : a)'

### Hint 21.18, untypeable term (with type: b) 'x'

### Hint 22.18,

in type of '(op branch : forall a : Type . (Nat ->? CTree a) -> CTree a)'

typename 'CTree' (7.16)

is not unifiable with type 'Tree a' (20.10)

### Hint 22.25,

in type of '(var s : b -> List (Tree a b))'

typename 'List' (20.58)

is not unifiable with type 'Tree a' (20.10)

### Hint 22.25, untypeable term (with type: a -> Tree a b) 's'