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

[Dominic Mulligan]

> a) ideally, Exference would take into account all locally defined (or
> even all visible) functions. This is problematic, as one generally has
> to be careful adding too many / the wrong functions to the environment
> because it can blow up the search space. There might be some
> heuristics to determine what can safely be added; alternatively the
> user could selectively add functions.

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.

Have you seen the recent announcement of Mote, a Vim plugin trying to
replicate something akin to Agda-mode for Haskell?

https://github.com/imeckler/mote

It seems that marrying these two projects, extending Mote with a
search facility based on exference, would be a good idea?