free type

Tree(a : Type) ::= 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

. (op caseTree : Tree Nat -> Tree Nat) (var t : Tree Nat) =

(case (var t : Tree Nat) of

(op EmptyLeaf[Nat] : forall a : Type . Tree a) ->

(op EmptyLeaf[_v17] : forall a : Type . Tree a) |

(op Leaf[Nat] : forall a : Type . a -> Tree a) (var n : Nat) ->

(op EmptyLeaf[_v17] : forall a : Type . Tree a) |

(op Node[Nat] : forall a : Type . Tree a -> a -> Tree a)

(op EmptyLeaf[Nat] : forall a : Type . Tree a)

(var n : Nat)

-> (op EmptyLeaf[_v17] : forall a : Type . Tree a) |

(op Node[Nat] : forall a : Type . Tree a -> a -> Tree a)

((op Node[Nat] : forall a : Type . Tree a -> a -> Tree a)

(var h : Tree Nat)

(var n : Nat))

(var n : Nat)

-> (var h : Tree Nat) |

(op Node[Nat] : forall a : Type . Tree a -> a -> Tree a)

((op Leaf[Nat] : forall a : Type . a -> Tree a) (var n : Nat))

(var n : Nat)

-> (op Leaf[Nat] : forall a : Type . a -> Tree a) (var n : Nat))

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