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
treebf1fbb4c2c885c84ebc064c93a0737da79ab16b3
parent8e841d13a36cc57300a3fe4eec5305b684212e60
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