diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 09:02:06 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 09:02:06 +0100 |
| commit | c63ff4179147ab237afe7d21d9e3740737c9b942 (patch) | |
| tree | 0fb4defb70302a2cba13b6f75f82fac39f15514e /Everything.agda | |
| parent | 26e2fea33aae257440e5571fb3f7e784938403e0 (diff) | |
| download | bidiragda-c63ff4179147ab237afe7d21d9e3740737c9b942.tar.gz | |
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.
Diffstat (limited to 'Everything.agda')
0 files changed, 0 insertions, 0 deletions