From dab051e89bbe904587a047d239e79610554d5c91 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 08:17:41 +0100
Subject: 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.
---
 Everything.agda | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Everything.agda')

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
-- 
cgit v1.2.3