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

Dominic Mulligan dominic.p.mulligan at googlemail.com
Mon Apr 27 09:23:11 UTC 2015

> 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?


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

More information about the Haskell-Cafe mailing list