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;

%% Type Constructors -----------------------------------------------------

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

Tree

: Type -> Type

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

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

%% Assumptions -----------------------------------------------------------

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

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

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

Suc : Nat -> Nat %(constructor)%

Zero : Nat %(constructor)%

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

%% Variables -------------------------------------------------------------

h : Tree Nat

n : Nat

t : Tree Nat

%% Sentences -------------------------------------------------------------

free type Tree(a : Type) ::=

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

free type Nat ::= Suc (Nat) | Zero %(ga_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

%% Diagnostics -----------------------------------------------------------

*** 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'