[Agda] Indentation for abstract and private declarations

Guillaume Brunerie guillaume.brunerie at gmail.com
Thu Oct 11 16:34:40 CEST 2012

I have a very practical question about indentation and emacs
interaction with Agda.
Suppose I have a program spanning several lines:

> program : type
> program = something
>   something-else
>   again-something-else

(lines 3 and 4 are indented with two spaces)

Now I decide that I want it to be abstract (or private).
What sequence of key-press am I supposed to do?

If I simply add a line "abstract" at the beginning, this doesn’t work
because the next two lines want to be indented more than the
"abstract" line.
If I indent the next two lines with two spaces, this doesn’t work
either because the two lines after that will want to be indented even

1. I can indent the first two lines with only one space, but one-space
indentation is a bit weird
2. I can indent the first two lines with two spaces and the subsequent
lines with four spaces, but this also looks weird because it doesn’t
match the rest of the file and I haven’t found an easy way to indent a
block of code (select + tab doesn’t work, so I usually use an emacs
macro to add two spaces at the beginning of each line, but this seems

Also, would it be possible to be able to define abstract or private
terms without having to indent everything further ?



More information about the Agda mailing list