summaryrefslogtreecommitdiff
path: root/FinMap.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-17 11:04:51 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-17 11:17:01 +0100
commit1561b1288b93c1353972d08e91f02101b2ccebfc (patch)
treed0c1e18521af040efffaf9019a8287a369ed1000 /FinMap.agda
parent248dc87e7c282a56bcc13fc28701a572288bc3ec (diff)
parentce4bbcc0c06b088a10881fcd66da5422571e7995 (diff)
downloadbidiragda-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 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions