std-lib: add indexed containers

[UlfNorell]

From stevan.a...@gmail.com on November 20, 2013 16:53:35

This series of patches adds indexed containers.

They can be applied in the following order (sorry for the Swedish, copy-pasted from an email I sent directly to Nisse a while ago):

agda-stdlib-unary: Medelstor, lägger till en del kombinatorer i relation.unary.

agda-stdlib-pointwise-iso: Liten, lägger till pointwise iso i function.inverse.

agda-stdlib-kleisli-composition: Liten, lägger till Kleisli composition i category.monad.indexed.

agda-stdlib-pred-transformers: Medelstor, lägger till predicate transformers (Pred I -> Pred O); i princip en pointwise version av relation.unary.

agda-stdlib-predicate-stuff: Stor, lägger till category.{functor,applicative,monad}.predicate. Dessa agerar på Pred I till skillnad ifrån category.*.indexed som agerar på Set men är indexerade.

agda-stdlib-indexed-containers: Stor, lägger till indexed containers core (som används i indexed container samt indexed W/M-types modulerna), indexed container combinatorer, samt free monads över indexed containers.

Attachment: agda-stdlib-unary.patch agda-stdlib-pointwise-iso.patch agda-stdlib-kleisli-composition.patch agda-stdlib-pred-transformers.patch agda-stdlib-predicate-stuff.patch agda-stdlib-indexed-containers.patch

Original issue: http://code.google.com/p/agda/issues/detail?id=973

[UlfNorell]

From andreas....@gmail.com on November 21, 2013 14:19:04

Labels: Type-Patch