[Agda] Setoid for List

[Joachim Breitner]

Hi,

Am Mittwoch, den 09.01.2013, 14:28 +0400 schrieb Serge D. Mechveliani:
> I fear I would need to set some similar code.
> But it is desirable to have such in the Standard Library for Agda.
> Say,  Setoid, DecSetoid, TotalOrder ...  for  Product, List, Vector
> -- these instances are very generic and fundamental.

to me it rather seems that there is a need for some generic programming,
i.e. a solution that works for all algebraic data types, or at least for
simple enough ones such as List or the simple data type Gen in
http://darcs.nomeata.de/agda-free-groups/Generators.agda
to avoid the boiler-plate code shown there.

Given that, instances for the data types in the standard library should
of course be included there.

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
  mail at joachim-breitner.de  |  nomeata at debian.org  |  GPG: 0x4743206C
  xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130109/3cdd993b/attachment.bin