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

Age	Commit message (Collapse)	Author
2012-10-22	now parameterize BFF	Helmut Grohne
	And update Bidir and Precond, cause they import BFF.
2012-10-22	also parameterize Precond	Helmut Grohne
	The import of CheckInsert was broken in previous commit.
2012-09-27	move definition of get-type to BFF and use it everywhere	Helmut Grohne

2012-09-26	rename suc-\== to suc-injective	Helmut Grohne
	This way of naming things is more similar to the standard library and to my own \::-injective. Suggested by Andres Loeh.
2012-09-08	give a sufficient precondition for theorem-2	Helmut Grohne
	If get on Fin results in Vecs whose elements are unique, then theorem-2 can be applied.