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 /Everything.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 'Everything.agda')
| -rw-r--r-- | Everything.agda | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda index 7383dd5..5ca5550 100644 --- a/Everything.agda +++ b/Everything.agda @@ -3,6 +3,7 @@ module Everything where import Generic import Structures +import Instances import FinMap import CheckInsert import GetTypes |