projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8e841d1) | patch
introduce denumerate
authorHelmut Grohne <helmut@subdivi.de>
Thu, 9 Feb 2012 10:58:54 +0000 (11:58 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 9 Feb 2012 10:58:54 +0000 (11:58 +0100)
commiteb6be3f9358e441fcee9256da5aae8915453f0a5
treebf1fbb4c2c885c84ebc064c93a0737da79ab16b3tree | snapshot
parent8e841d13a36cc57300a3fe4eec5305b684212e60commit | diff
introduce denumerate

It is some kind of counter part to enumerate. That is:

map (denumerate s) (enumerate s) \== s

It can be employed in bff and I believe it to simplify reasoning on bff.
Bidir.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)