LiftGet: replace vec-length-same with toList-subst
authorHelmut Grohne <helmut@subdivi.de>
Tue, 11 Sep 2012 21:33:29 +0000 (23:33 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 11 Sep 2012 21:33:29 +0000 (23:33 +0200)
commitd3f12c72cb10462ac5ebce3a8cda462c70bff3d9
treee8de507287efc13ebbf8c9e614d1b79fdf76fab8
parent6aba617941bc5e66f414846131a3e02d9ae1fc41
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.
LiftGet.agda