[Agda] Abbreviation mode

Robin Green greenrd at greenrd.org
Fri Oct 2 16:38:04 CEST 2009


Two points about abbrev-mode:

The instructions on the wiki at
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Abbreviation
don't work - the ' and " characters have been turned into so-called
"Smart Quotes", which confuses emacs.

Also, the "Agda2 Mode Abbrevs Use Defaults:" option should probably
default to No.

How does one use the default abbreviations if that option is turned
off, by the way?

-- 
Robin


More information about the Agda mailing list