LiftGet: vec-length is also known as subst (Vec A)
authorHelmut Grohne <helmut@subdivi.de>
Mon, 10 Sep 2012 20:34:16 +0000 (22:34 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Mon, 10 Sep 2012 20:34:16 +0000 (22:34 +0200)
commit6aba617941bc5e66f414846131a3e02d9ae1fc41
treefdd7bbde53b59b63a9ed16b9212d24aff9506d51
parentbd2a63675bb859e42d9e1464ff9a7883884c1fd5
LiftGet: vec-length is also known as subst (Vec A)

Thanks to Andres Löh for spotting.
LiftGet.agda