[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