At 2015-02-13T13:29:50Z, gallais wrote: > Would it be welcomed to add these to the standard agda-mode? I'd welcome it for sure! It may provoke people to find mo' better indentation rules. Cheers, Raghu. -- N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/ Harish-Chandra Research Institute, http://www.hri.res.in/