Merge branch feature-partial-getlen into master
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 17 Feb 2014 10:04:51 +0000 (11:04 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 17 Feb 2014 10:17:01 +0000 (11:17 +0100)
commit1561b1288b93c1353972d08e91f02101b2ccebfc
treed0c1e18521af040efffaf9019a8287a369ed1000
parent248dc87e7c282a56bcc13fc28701a572288bc3ec
parentce4bbcc0c06b088a10881fcd66da5422571e7995
Merge branch feature-partial-getlen into master

It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.

Conflicts: heavy
BFF.agda (imports, bff type clash)
Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
                    lemma-get-mapMV)
Generic.agda (imports)
Precond.agda (imports, bff type clash in assoc-enough)
BFF.agda
Bidir.agda
Generic.agda
Precond.agda