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
tree5ae83b04ae794d61ddcdf18e58435fbce95cd9f8
parent84231ed91ae814d5a256e5fa24810c886ae31369
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