remove VecRevBFF
authorHelmut Grohne <helmut@subdivi.de>
Fri, 5 Oct 2012 08:58:15 +0000 (10:58 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 5 Oct 2012 08:58:15 +0000 (10:58 +0200)
commit96e45ecbf31c5685fa914882ec4b21b1392c49fc
tree361c0c2ece69db38604b874f20cb93a7e68507c0
parentcaeae59c7e6ae461a066ac008160035dbff9122b
remove VecRevBFF

The case is not interesting, because it is too restricted. The defined
get-type requires a bijection between input length and output length.
Since it requires polymorphism we get a reverse get-len via free
theorems and both compositions are required to be identities. Thus the
case is restricted without providing new insights.
BFF.agda