diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 14:04:29 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 14:04:29 +0100 |
| commit | ffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf (patch) | |
| tree | f7fc1e1683c5cbb9d665cbcd1215a81ce041b47c /GetTypes.agda | |
| parent | 934f2003d4f47c2af3a91cd827d75caeded7ec7a (diff) | |
| download | bidiragda-ffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf.tar.gz | |
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.
Diffstat (limited to 'GetTypes.agda')
0 files changed, 0 insertions, 0 deletions