CTree.hascasl revision 20921b0900acb7e19a778e4b309a7e6d6c305e5e
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervars a,b: Type
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedergenerated type Set a ::= empty | add a (Set a)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedergenerated type Sys b ::= node b (Set (Sys b))
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedertype Nat
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedervar a: Type
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedergenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type L ::= abs (L -> L)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type Tree a b ::= leaf b | branch (a -> Tree a b)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
20921b0900acb7e19a778e4b309a7e6d6c305e5eChristian Maederfree type List a ::= nil | cons (a; List a)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type Tree a b ::= leaf a | branch (b -> List (Tree a b))
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervar c : Type
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervars f : a -> c; g : (b -> List c) -> c; x : a; s : b -> List (Tree a b)
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder. fold f g (leaf x) = f x
453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder. def (fold f g (branch s))