| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-01-27 | cleanup unused functions and useless steps | Helmut Grohne | |
| 2014-01-24 | prove theorem-2 in the presence of delete | Helmut Grohne | |
| The biggest piece of this puzzle was establishing get <$> mapMV f v == mapMV f (get v) provided that the result of mapMV is just something. lemma-union-not-used lost a "map just", but could be retained in structure. | |||
| 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