diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-11 23:33:29 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-11 23:33:29 +0200 |
| commit | d3f12c72cb10462ac5ebce3a8cda462c70bff3d9 (patch) | |
| tree | e8de507287efc13ebbf8c9e614d1b79fdf76fab8 /FreeTheorems.agda | |
| parent | 6aba617941bc5e66f414846131a3e02d9ae1fc41 (diff) | |
| download | bidiragda-d3f12c72cb10462ac5ebce3a8cda462c70bff3d9.tar.gz | |
LiftGet: replace vec-length-same with toList-subst
The name vec-length-same hides the fact that it eliminates a toList and
a fromList. Actually a more generic form without fromList is possible.
Thanks to Joachim Breitner for spotting.
Diffstat (limited to 'FreeTheorems.agda')
0 files changed, 0 insertions, 0 deletions