| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-02-24 | define mapMV via sequenceV | Helmut Grohne |
| 2014-02-17 | Merge branch feature-partial-getlen into master | Helmut Grohne |
| 2014-02-07 | eliminate useless withs | Helmut Grohne |
| 2014-02-07 | replace rewrite with cong where feasible | Helmut Grohne |
| 2014-02-03 | make things compile with 2.3.0.1 | Helmut Grohne |
| 2014-01-30 | express VecBFF via PartialVecBFF | Helmut Grohne |
| 2014-01-28 | improve readability using _∋_≈_ instead of Setoid._≈_ | Helmut Grohne |
| 2014-01-28 | use the indexed version of the Vec Setoid | Helmut Grohne |
| 2014-01-27 | Merge branch feature-delete | Helmut Grohne |
| 2014-01-27 | cleanup unused functions and useless steps | Helmut Grohne |
| 2014-01-24 | prove theorem-2 in the presence of delete | Helmut Grohne |
| 2014-01-17 | show that Vec is an indexed Setoid | Helmut Grohne |
| 2014-01-16 | generalize lemma-insert-same to arbitrary Setoids | Helmut Grohne |
| 2013-12-16 | add a mapM variant on the Maybe monad on Vecs | Helmut Grohne |
| 2013-12-16 | move generic functions to a new Generic module | Helmut Grohne |
 |
index : ~helmut/bidiragda.git | |
| Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf) | Helmut Grohne |
| summaryrefslogtreecommitdiff |
path: root/Generic.agda