diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-06-19 16:28:03 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-06-19 16:28:03 +0200 |
| commit | 61d74dd8e6cffd27e53a1a93c5560bbdf346941f (patch) | |
| tree | 5ae83b04ae794d61ddcdf18e58435fbce95cd9f8 /LiftGet.agda | |
| parent | 84231ed91ae814d5a256e5fa24810c886ae31369 (diff) | |
| download | bidiragda-61d74dd8e6cffd27e53a1a93c5560bbdf346941f.tar.gz | |
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
Diffstat (limited to 'LiftGet.agda')
0 files changed, 0 insertions, 0 deletions