implement a bff on a shaped source type
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 10 Mar 2014 07:17:41 +0000 (08:17 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 10 Mar 2014 07:17:41 +0000 (08:17 +0100)
commitdab051e89bbe904587a047d239e79610554d5c91
treeecbcb94e559396d2f2546003d0843fa1da1016bb
parent3616445f9a60402701ca00a22e9e6e2fbe95c741
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.
BFF.agda
Everything.agda
GetTypes.agda
Instances.agda [new file with mode: 0644]
Structures.agda