[Haskell-cafe] ANN: exference: a different djinn
lsp at informatik.uni-kiel.de
Mon Apr 27 12:14:15 UTC 2015
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.
More information about the Haskell-Cafe