b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskifree type Tree a ::= Leaf a | Node (Tree a) a | EmptyLeaf

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerfree type Nat ::= Zero | Suc Nat

876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maederop caseTree : forall a . Tree Nat -> Tree Nat

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiforall h : Tree Nat; n : Nat; t : Tree Nat

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu. (op caseTree : Tree Nat -> Tree Nat) (var t : Tree Nat) =

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski (case (var t : Tree Nat) of

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

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

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

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

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

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

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski (var n : Nat)

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

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

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

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski (var h : Tree Nat)

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski (var n : Nat))

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowski (var n : Nat)

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -> (var h : Tree Nat) |

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

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

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa (var n : Nat)

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

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski%% Type Constructors -----------------------------------------------------

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskiNat

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski: Type

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder %[free type Nat ::=

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Zero : Nat

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Suc : Nat -> Nat(Nat)]%

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till MossakowskiTree

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa: Type -> Type

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

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Leaf : a -> Tree a(a)

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

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski EmptyLeaf : Tree a]%

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder%% Assumptions -----------------------------------------------------------

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederEmptyLeaf : forall a : Type . Tree a %(construct Tree)%

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederLeaf : forall a : Type . a -> Tree a %(construct Tree)%

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

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskiSuc : Nat -> Nat %(construct Nat)%

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederZero : Nat %(construct Nat)%

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskicaseTree : Tree Nat -> Tree Nat %(op)%

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski%% Variables -------------------------------------------------------------

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowskih : Tree Nat

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowskin : Nat

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowskit : Tree Nat

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder%% Sentences -------------------------------------------------------------

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederfree type Tree(a : Type) ::=

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Leaf : a -> Tree a(a)

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder Node : Tree a -> a -> Tree a(Tree a)(a)

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till Mossakowski EmptyLeaf : Tree a %(ga_Tree)%

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederfree type Nat ::=

dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder Zero : Nat

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder Suc : Nat -> Nat(Nat) %(ga_Nat)%

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercaseTree t =

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder(case t of

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski EmptyLeaf -> EmptyLeaf |

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Leaf n -> EmptyLeaf |

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski Node EmptyLeaf n -> EmptyLeaf |

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Node (Node h n) n -> h |

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski Node (Leaf n) n -> Leaf n)

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski%% Diagnostics -----------------------------------------------------------

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder### Warning 1.18, missing kind for type variable 'a'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder### Warning 4.23, missing kind for type variable 'a'

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

e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder a in 'Tree Nat -> Tree Nat'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder### Hint 6.9, not a kind 'Tree Nat'

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

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder### Hint 7.16, not a kind 'Tree Nat'

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder### Hint 10.27, rebound variable 'n'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski### Hint 11.37, rebound variable 'n'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski### Hint 12.33, rebound variable 'h'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski### Hint 12.35, rebound variable 'n'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski### Hint 12.37, rebound variable 'n'

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder### Hint 13.33, rebound variable 'n'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski### Hint 13.36, rebound variable 'n'

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski