[Agda] Proposed minor additions to standard library

[Gregory Crosswhite]

Hey everyone,

I would like to propose the following minor additions to the standard library:

    1) Adding a function mapDec to Relation.Nullary that allows users to change between types Dec A to Dec B given maps (A -> B) and (B -> A).
    2) Creating a module for ExpFunctors -- that is, invariant functors which can take you between F A to F B if you have maps (A -> B) and (B
-> A).
    3) Make Dec a ExpFunctor by adding an appropriate record to Relation.Nullary that makes use of mapDec.

I've attached a tarball with patches (make via. darcs send --output=X.patch) to implement these changes.  The file mapDec.patch contains a patch to implement change 1.  The file ExpFunctor.patch contains a patch to implement change 2.  Since darcs won't let me send a patch for change 3 in isolation since it depends on changes 1 and 2, the file DoEverything.patch contains a patch for each of the three changes.

Feedback is welcome.

Cheers,
Greg

PS:  To the moderator, this e-mail is a resubmission of an earlier e-mail but with the patches gzipped to keep its size down.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: patches.tar.gz
Type: application/gzip
Size: 9357 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100913/63ceafef/patches.tar-0001.bin