CTree.hascasl revision 20921b0900acb7e19a778e4b309a7e6d6c305e5e
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringvars a,b: Type
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringgenerated type Set a ::= empty | add a (Set a)
12b42c76672a66c2d4ea7212c14f8f1b5a62b78dTom Gundersengenerated type Sys b ::= node b (Set (Sys b))
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringtype Nat
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringvar a: Type
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringgenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringfree type L ::= abs (L -> L)
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringfree type Tree a b ::= leaf b | branch (a -> Tree a b)
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringfree type List a ::= nil | cons (a; List a)
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringfree type Tree a b ::= leaf a | branch (b -> List (Tree a b))
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringvar c : Type
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poetteringvars f : a -> c; g : (b -> List c) -> c; x : a; s : b -> List (Tree a b)
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering. fold f g (leaf x) = f x
56ba3c78ae35065064c4289a0c8e22a81256af20Zbigniew Jędrzejewski-Szmek. def (fold f g (branch s))
8e129f5156569e1bc858b002ca54cd447c38f4f1Lennart Poettering