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

Age	Commit message (Collapse)	Author
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