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 ::=

Zero : Nat

Suc : Nat -> Nat(Nat)]%

Tree

: Type -> Type

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

Leaf : a -> Tree a(a)

Node : Tree a -> a -> Tree a(Tree a)(a)

EmptyLeaf : Tree a]%

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

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

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

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

Suc : Nat -> Nat %(construct Nat)%

Zero : Nat %(construct Nat)%

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

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

h : Tree Nat

n : Nat

t : Tree Nat

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

free type Tree(a : Type) ::=

Leaf : a -> Tree a(a)

Node : Tree a -> a -> Tree a(Tree a)(a)

EmptyLeaf : Tree a %(ga_Tree)%

free type Nat ::=

Zero : Nat

Suc : Nat -> Nat(Nat) %(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 -----------------------------------------------------------

### Warning 1.18, missing kind for type variable 'a'

### Warning 4.23, missing kind for 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'