[Haskell-cafe] Re: [Haskell] Re: Announcing Djinn, new version 2004-12-13

[Lennart Augustsson]

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 <lennart at augustsson.net> wrote in article <439F4539.4070205 at 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
>