I came across an example in which the case-splitting is similar to the Majority Function.
f :: Nat -> Nat -> Nat -> Nat f 0 0 0 = 1 f 0 (succ y) z = g1 y z f (succ x) y 0 = g2 x y f x 0 (succ z) = g3 x z f (succ x) (succ y) (succ z) = f (succ x) (succ y) z + f (succ x) y (succ z) + f x (succ y) (succ z) where g1 g2 and g3 were defined beforehand. As we discussed before, this kind of functions cannot be defined by the eliminator (of Nat) to satisfy every equation computationally. We have to modify the function to the one that has 8 cases. However, if we don't care whether it is total (ie, if we allow partially defined function), then it can be defined as it is. Cheers, Yong ============================== Dr. Yong Luo Computing Laboratory University of Kent