pass get functions as records
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 08:02:06 +0000 (09:02 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 08:02:06 +0000 (09:02 +0100)
commitc63ff4179147ab237afe7d21d9e3740737c9b942
tree0fb4defb70302a2cba13b6f75f82fac39f15514e
parent26e2fea33aae257440e5571fb3f7e784938403e0
pass get functions as records

This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.
BFF.agda
Bidir.agda
FreeTheorems.agda
LiftGet.agda
Precond.agda