[Agda] ANN: agda-move-improvements-0.3

Wojciech Jedynak wjedynak at gmail.com
Sun Jun 12 12:28:09 CEST 2011


Hello everybody!

This is a follow-up to those ANNs:
* ANN: coq-like agda-mode support for databases of lemmas
(http://article.gmane.org/gmane.comp.lang.agda/2911)
* ANN: convenient way to add a with expression from a goal
(http://article.gmane.org/gmane.comp.lang.agda/2928)

I decided to collect all of my changes under the name of agda-mode-improvements.
The code can be found at https://github.com/wjzz/Agda-mode-improvements

Since the last release I've implemented importing and listing contents
of databases, fixed some bugs and created two simple features:
- generating a function body stub based on type signature
- deleting a broken pattern declaration and inserting '... | '

The details about the new features can be found here:
https://github.com/wjzz/Agda-mode-improvements/blob/master/README

A changelog is also available:
https://github.com/wjzz/Agda-mode-improvements/blob/master/changes.txt

An updated tutorial on lemma databases can found at:
https://github.com/wjzz/Agda-mode-improvements/blob/master/LemmaDatabaseTutorial.lagda

Greetings,
Wojciech Jedynak (wjzz)


More information about the Agda mailing list