[Agda] Indentation in stdlib files
Andreas Abel
abela at chalmers.se
Fri Feb 13 08:19:44 CET 2015
To align at ":" I use the align-regexp command of emacs. (Of course, it
is not restricted to ":"...)
Mark a region
M-x align-regexp RET
: RET
Cheers,
Andreas
On 13.02.2015 07:08, N. Raghavendra wrote:
> Hi,
>
> I was wondering how to get the nice indentation and alignment which is
> seen in stdlib files. E.g.,
>
> --8<---------------cut here---------------start------------->8---
> record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
> infixl 7 _∙_
> infix 4 _≈_
> field
> Carrier : Set c
> _≈_ : Rel Carrier ℓ
> _∙_ : Op₂ Carrier
> isSemigroup : IsSemigroup _≈_ _∙_
>
> open IsSemigroup isSemigroup public
>
> setoid : Setoid _ _
> setoid = record { isEquivalence = isEquivalence }
> --8<---------------cut here---------------end--------------->8---
>
> The 7 and 4 in the infix statements are aligned with each other. All
> the colons in the field statements are aligned with each other. Is
> there some Emacs variable/command which does this? Can one use
> haskell-stylish with Agda?
>
> Thanks,
> Raghu.
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list