projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c62e107) | patch
replace idrange with enumerate
authorHelmut Grohne <helmut@subdivi.de>
Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)
commit8e841d13a36cc57300a3fe4eec5305b684212e60
tree2f8cebdba6c2b4ecbb6d9804a7acd20e96dacf34tree | snapshot
parentc62e107155b8fea28dbf1637f9187e4f24f75173commit | diff
replace idrange with enumerate

Looks like uses of idrange would always be passed a length, so move it
inside the definition.
Bidir.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)