diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-03-10 08:17:41 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-03-10 08:17:41 +0100 |
| commit | dab051e89bbe904587a047d239e79610554d5c91 (patch) | |
| tree | ecbcb94e559396d2f2546003d0843fa1da1016bb /Precond.agda | |
| parent | 3616445f9a60402701ca00a22e9e6e2fbe95c741 (diff) | |
| download | bidiragda-dab051e89bbe904587a047d239e79610554d5c91.tar.gz | |
implement a bff on a shaped source type
Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.
Diffstat (limited to 'Precond.agda')
0 files changed, 0 insertions, 0 deletions