~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-10-14	drop the injection requirement for gl₁	Helmut Grohne
	Turns out, we never use this requirement. The only place where it may come in relevant is the free theorems. But here non-injectivity turns out to be reasoning about multiple get functions that are selected by the additional index each individually satisfying the free theorem and thus commonly satisfying it as well.
2014-06-06	drop-suc is cong pred	Helmut Grohne

2014-03-10	Example: show that PairVec is Shaped	Helmut Grohne
	Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s) is not Shaped in this way since its real index is only a number.
2014-02-24	add intersperse as another example	Helmut Grohne

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-10	add sieve to examples	Helmut Grohne

2014-02-05	add examples	Helmut Grohne