[Agda] deriving Eq for Agda?

[Vilhelm Sjöberg]

Dear Agda list,

in Haskell I can say "deriving Eq" and in Coq "decide equality". Is there a
similar automated tool for creating equality decision procedures for Agda
inductive types?

Failing that, is there a recommended idiomatic way of writing them, and do you
know of any elegant examples? Each time I've tried to write one it seems quite
ungainly and ad-hoc.

Thanks,
  Vilhelm