projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 84231ed) | patch
third definition of bff
authorHelmut Grohne <helmut@subdivi.de>
Tue, 19 Jun 2012 14:28:03 +0000 (16:28 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 19 Jun 2012 14:28:03 +0000 (16:28 +0200)
commit61d74dd8e6cffd27e53a1a93c5560bbdf346941f
tree5ae83b04ae794d61ddcdf18e58435fbce95cd9f8tree | snapshot
parent84231ed91ae814d5a256e5fa24810c886ae31369commit | diff
third definition of bff

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
BFF.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)