1 --!! TEST OF DEFACTORISATION FOR FUNCTIONS THAT DROP
2 --!! POLYMORPHIC VARIABLES
6 data Pair a b = MkPair a b
7 data LList alpha = Nill | Conss alpha (LList alpha)
8 data Nat = Zero | Succ Nat
9 data Tree x = Leaf x | Node (Tree x) (Tree x)
10 data A a = MkA a (A a)
12 append :: LList a -> LList a -> LList a
13 append xs ys = case xs of
15 Conss z zs -> Conss z (append zs ys)
17 -- The following function drops @b@.
19 flat :: Tree (Pair a b) -> LList a
21 Leaf (MkPair a b) -> Conss a Nill
22 Node l r -> append (flat l) (flat r)
24 fl :: Boolean -> LList Boolean
25 fl x = flat (Leaf (MkPair TT Zero))