[Haskell-cafe] ANN: exference: a different djinn

[lennart spitzner]

On 27/04/15 11:23, Dominic Mulligan wrote:
> Is this a major problem?  As far as I can tell Agda's automated proof
> search does not take into account any globally defined functions or
> constants and yet is still (moderately) useful.

No, i just have high expectations :)
Even with just the current functionality, if there is a typed hole
in an expression like `f = _ x y` if the user knows that the
implementation will involve some specific global function bar, she
could write `f = _ bar x y`.

> Have you seen the recent announcement of Mote, a Vim plugin trying to
> replicate something akin to Agda-mode for Haskell?
> It seems that marrying these two projects, extending Mote with a
> search facility based on exference, would be a good idea?

In a way it even inspired me to (finally) make the announcement. I
have not, but will try to find time to play with Mote in the next days.