Well, the proof search is terminating (and complete) so it has to stop somewhere. That happens to be result with this particular search strategy. -- Lennart Chung-chieh Shan wrote:

Lennart Augustsson wrote in article <439F4539.4070205@augustsson.net> in gmane.comp.lang.haskell.general:

...

There is a new version of Djinn available, with two notable new features: Haskell data types can be defined and the found functions are sorted (heuristically) to present the best one first.

Hello,

I wonder why the only Church numerals Djinn found were 0 and 1?

Djinn> :set +m Djinn> num ? (a -> a) -> (a -> a) num :: (a -> a) -> a -> a num x1 x2 = x1 x2 -- or num _ x2 = x2

Very cool, in any case.

Ken