projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 19670ab) | patch
add a GetV-to-GetL transformer
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 3 Feb 2014 10:41:14 +0000 (11:41 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 3 Feb 2014 10:41:14 +0000 (11:41 +0100)
commitfd78e72b45e3e78286f2c68d2abe743da0171c90
tree2109415a43946ddd2ba485a953f91252c2f62543tree | snapshot
parent19670abeff9895de593ef26ad2da247ae590ce90commit | diff
add a GetV-to-GetL transformer

This is an improved version of getVec-to-getList in that it also
transports the corresponding free theorem.
LiftGet.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)