[Agda] Indentation for abstract and private declarations

Andreas Abel andreas.abel at ifi.lmu.de
Thu Oct 11 16:56:34 CEST 2012

To indent a selected block in Emacs by 2 spaces, press

   C-u 2 C-x C-i

(C-i is the same as TAB).  Alternatively, use the rectangle command

   C-x r t SPC SPC RET

(which can be used to replace a rectangle (which can have width 0) by a 
rectangle of the same height with identical text in each line).

Unfortunately, "abstract" is not available as a modifier for an 
identifier, like in

   abstract program : type
   program = ...

"abstract" always expects a block, and this has to be indented.


On 11.10.2012 16:34, Guillaume Brunerie wrote:
> Hello,
> 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
> further
> 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
> overkill)
> Also, would it be possible to be able to define abstract or private
> terms without having to indent everything further ?
> Thanks,
> Guillaume
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list