make the getlen functions explicit in PartialVecBFF
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 13:04:29 +0000 (14:04 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 13:04:29 +0000 (14:04 +0100)
commitffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf
treef7fc1e1683c5cbb9d665cbcd1215a81ce041b47c
parent934f2003d4f47c2af3a91cd827d75caeded7ec7a
make the getlen functions explicit in PartialVecBFF

There is no way for Agda to infer these functions or even the intended
index Setoid, so making these explicit is rather required.
BFF.agda