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
tree2f8cebdba6c2b4ecbb6d9804a7acd20e96dacf34
parentc62e107155b8fea28dbf1637f9187e4f24f75173
replace idrange with enumerate

Looks like uses of idrange would always be passed a length, so move it
inside the definition.
Bidir.agda