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

Age	Commit message (Collapse)	Author
2015-06-09	drop the Function.Equality requirement from GetTypes	Helmut Grohne
	We never used the equality property. Thus a simple function is sufficient here. We always fulfilled the property using ≡-to-Π anyway.
2014-09-26	resolve ambiguity in BFFPlug	Helmut Grohne
	Fixes compilation with Agda 2.4.2.
2014-02-26	remove the sequenceV call from bff	Helmut Grohne
	This allows bff to be more precise with regard to its failure modes, even though we are not yet making use of that projected precision. It allows inserting a default value for entries that could not be recovered in a shape changing update as described in VoigtlaenderHMW13.
2014-02-17	use drop, tail and take from Data.Vec in examples	Helmut Grohne
	This is possible using the PartialVecVec implementation.
2014-02-17	switch examples to PartialVecVec	Helmut Grohne

2014-02-14	add back original bff function before shape updates	Helmut Grohne

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.