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.