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

[Wojciech Jedynak]

( Sorry for the noise, when I check the archive at
https://lists.chalmers.se/pipermail/agda/2011/thread.html it seems
that the previous message body was truncated, so I'm trying again,
this time without any attachments... )

My original mail:
-----------------------

Hello everybody!

I'm a Coq user that has been recently fascinated by Agda. As I started
to make some simple developments, I realized that being able to extend
the behavior of auto by using databases of user selected lemmas (the
way it works in Coq) would be pretty nice to have. I haven't seen
anything like this on the Agda wiki, so I tried to implement a simple
and straightforward prototype in emacs-lisp by extending the
agda-mode. Basically I just modified the agda2-mode.el file, so I'm
taking the liberty of attaching the extended version to this mail.

This implementation might occur to be a little simplistic to you, but
since I didn't touch the Haskell source files, it's very easy to
install and it's pretty lightweight.
As I'm not very experienced with writing in elisp there may be some
rough edges, but I tried to comment some potential pitfalls. I have
only tested this with Agda 2.2.10.

To see what it's all about please check the Tutorial.lagda file at my
git repository (https://github.com/wjzz/Agda-mode-improvements) and
read it there.
I may have written too many details, but I hope this way it will be
useful even to beginners.

I have some ideas for improvement, but since I don't know if anybody
will be interested at all I decided to release this early version. I
hope you'll find it useful and since it's actually my first go at
contributing to an open-source project please don't hesitate to
comment on anything.

Greetings,
Wojtek Jedynak (wjzz)