[Agda] ANN: coq-like agda-mode support for databases of lemmas

[Nils Anders Danielsson]

On 2011-05-28 01:59, Wojciech Jedynak wrote:
> However, there seem to be more cons that pros.

I didn't mean to imply that this was a complete, polished
implementation. However, I don't think we should introduce a new
mechanism for naming and importing things.

By the way, you missed one disadvantage: including lemmas with initial
implicit arguments in databases is more complicated than one would want.

-- 
/NAD