diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-10-05 10:58:15 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-10-05 10:58:15 +0200 |
| commit | 96e45ecbf31c5685fa914882ec4b21b1392c49fc (patch) | |
| tree | 361c0c2ece69db38604b874f20cb93a7e68507c0 /Bidir.agda | |
| parent | caeae59c7e6ae461a066ac008160035dbff9122b (diff) | |
| download | bidiragda-96e45ecbf31c5685fa914882ec4b21b1392c49fc.tar.gz | |
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.
Diffstat (limited to 'Bidir.agda')
0 files changed, 0 insertions, 0 deletions