summaryrefslogtreecommitdiff
path: root/BFF.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-03 11:41:14 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-03 11:41:14 +0100
commitfd78e72b45e3e78286f2c68d2abe743da0171c90 (patch)
tree2109415a43946ddd2ba485a953f91252c2f62543 /BFF.agda
parent19670abeff9895de593ef26ad2da247ae590ce90 (diff)
downloadbidiragda-fd78e72b45e3e78286f2c68d2abe743da0171c90.tar.gz
add a GetV-to-GetL transformer
This is an improved version of getVec-to-getList in that it also transports the corresponding free theorem.
Diffstat (limited to 'BFF.agda')
0 files changed, 0 insertions, 0 deletions