~helmut/bidiragda.git - Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)

Age	Commit message (Collapse)	Author
2014-03-10	implement a bff on a shaped source type	Helmut Grohne
	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.
2014-03-07	add a Functor structure	Helmut Grohne
	The intent is to replace some uses of Vec with a structure that also happens to be a functor. RawFunctors from the standard library provide no laws though, so we define a Functor structure that adds the laws. As an additional law congruence is added, because * Other standard library structures in Algebra.Structures also require congruence. * Otherwise the identity law would have to reason about different identities.
2014-02-10	add bffplug and bffinv functions and examples	Helmut Grohne
	We can now exploit getlen being rightinvertible and it works for drop and sieve.
2014-02-05	add examples	Helmut Grohne

2014-01-30	allow importing of Bidir without any postulates	Helmut Grohne

2014-01-30	simplify compilation of the whole source	Helmut Grohne