free type Tree a ::= Leaf a | Node (Tree a) a | EmptyLeaf

free type Nat ::= Zero | Suc Nat

op caseTree : forall a . Tree Nat -> Tree Nat

forall h : Tree Nat; n : Nat; t : Tree Nat

. caseTree t

= case t of

EmptyLeaf -> EmptyLeaf |

Leaf n -> EmptyLeaf |

Node EmptyLeaf n -> EmptyLeaf |

Node (Node h n) n -> h |

Node (Leaf n) n -> Leaf n;

types

Nat : Type %[free type Nat ::= Suc (Nat) | Zero]%;

Tree

: Type -> Type

%[free type Tree(a : Type) ::=

EmptyLeaf | Leaf (a) | Node (Tree a) (a)]%

op EmptyLeaf : forall a : Type . Tree a %(constructor)%

op Leaf : forall a : Type . a -> Tree a %(constructor)%

op Node : forall a : Type . Tree a -> a -> Tree a %(constructor)%

op Suc : Nat -> Nat %(constructor)%

op Zero : Nat %(constructor)%

op caseTree : Tree Nat -> Tree Nat %(op)%

vars

h : Tree Nat;

n : Nat;

t : Tree Nat

free type Tree(a : Type) ::=

EmptyLeaf | Leaf (a) | Node (Tree a) (a) %(ga_Tree)%

free type Nat ::= Suc (Nat) | Zero %(ga_Nat)%

forall t : Tree Nat

. caseTree t

= case t of

EmptyLeaf -> EmptyLeaf |

Leaf n -> EmptyLeaf |

Node EmptyLeaf n -> EmptyLeaf |

Node (Node h n) n -> h |

Node (Leaf n) n -> Leaf n

*** Error 1.18, unknown type variable 'a'

*** Error 4.23, unknown type variable 'a'

### Warning 4.27-4.44, ignoring unused variable(s)

a in 'Tree Nat -> Tree Nat'

### Hint 6.9, not a kind 'Tree Nat'

### Hint 7.9, not a class 'Nat'

### Hint 7.16, not a kind 'Tree Nat'

### Hint 10.27, rebound variable 'n'

### Hint 11.37, rebound variable 'n'

### Hint 12.33, rebound variable 'h'

### Hint 12.35, rebound variable 'n'

### Hint 12.37, rebound variable 'n'

### Hint 13.33, rebound variable 'n'

### Hint 13.36, rebound variable 'n'