Very interesting! It got me thinking: if you combine this with the Arbitrary class [1] of QuickCheck you can use it check if you have defined a function that is "equal" to an already defined function. Let's say I write the following function: intMul ∷ Integer → Integer → Integer intMul x 0 = 0 intMul x n = x + intMul x (n - 1) No you can automatically apply this function to a list of 100 generated inputs to get a list of input output pairs. Feed this into haltavista and it should tell you that you can replace your definition with Prelude (*). While such an observation is certainly not a proof it is still useful. It would be a nice addition to a Haskell editor. Especially for those new to the language. Regards, Roel 1 - http://hackage.haskell.org/packages/archive/QuickCheck/2.3/doc/html/Test-Qui...