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

Nils Anders Danielsson nad at chalmers.se
Sat May 28 09:08:31 CEST 2011


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


More information about the Agda mailing list