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;
Tree : Type -> Type
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
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
1.18: *** Error: unknown type variable 'a'
4.23: *** Error: unknown type variable 'a'
4.27-4.46: ### Warning:
ignoring unused variable(s)
a in
'Tree Nat -> Tree Nat'
6.9: ### Hint: not a kind 'Tree Nat'
7.9: ### Hint: not a class 'Nat'
7.16: ### Hint: not a kind 'Tree Nat'
10.27: ### Hint: rebound variable 'n'
11.37: ### Hint: rebound variable 'n'
12.33: ### Hint: rebound variable 'h'
12.35: ### Hint: rebound variable 'n'
12.37: ### Hint: rebound variable 'n'
13.33: ### Hint: rebound variable 'n'
13.36: ### Hint: rebound variable 'n'