[Agda] Indentation in stdlib files

N. Raghavendra raghu at hri.res.in
Fri Feb 13 07:08:55 CET 2015


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.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/



More information about the Agda mailing list