| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2012-06-19 | third definition of bff | Helmut Grohne | |
| It is a definition based on Vec but with less assumptions. The VecBFF has therefore been renamed to VecRevBFF. VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m | |||
| 2012-06-05 | make the Vec bff more similar to the List version | Helmut Grohne | |
| 2012-06-05 | define a bff over Vec | Helmut Grohne | |
| 2012-06-05 | move bff and friends to submodule ListBFF | Helmut Grohne | |
 |
index : ~helmut/bidiragda.git | |
| Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf) | Helmut Grohne |
| summaryrefslogtreecommitdiff |