diff options
author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-17 11:04:51 +0100 |
---|---|---|
committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-17 11:17:01 +0100 |
commit | 1561b1288b93c1353972d08e91f02101b2ccebfc (patch) | |
tree | d0c1e18521af040efffaf9019a8287a369ed1000 /Examples.agda | |
parent | 248dc87e7c282a56bcc13fc28701a572288bc3ec (diff) | |
parent | ce4bbcc0c06b088a10881fcd66da5422571e7995 (diff) | |
download | bidiragda-1561b1288b93c1353972d08e91f02101b2ccebfc.tar.gz |
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)
Diffstat (limited to 'Examples.agda')
0 files changed, 0 insertions, 0 deletions