[Agda] deriving Eq for Agda?

[Nils Anders Danielsson]

On 2009-12-03 04:31, Vilhelm Sjöberg wrote:
> Failing that, is there a recommended idiomatic way of writing them
> [...]?

There are a number of brute-force examples in the standard library. See
Data.Bool._≟_ or Data.Nat._≟_, for instance.

Note that the brute-force technique requires a quadratic number of
constructors (if you want to prove correctness of your decision
procedure). In some cases it may be easier to provide an injection into
another type and use the decision procedure for that type instead. For
an example, see Mixfix.Fixity._≟_:

  http://www.cs.nott.ac.uk/~nad/listings/parser-combinators/Mixfix.Fixity.html

--
/NAD