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

Age	Commit message (Collapse)	Author
2012-10-22	finally parameterize CheckInsert	Helmut Grohne
	Also adapt depending modules. Long lines generally become shorter. The misleading name "EqInst" (hiding the decidability) got discarded.
2012-10-22	now parameterize BFF	Helmut Grohne
	And update Bidir and Precond, cause they import BFF.
2012-10-05	move all postulates to one module	Helmut Grohne
	This should make it easier to see what is assumed.
2012-10-05	remove VecRevBFF	Helmut Grohne
	The case is not interesting, because it is too restricted. The defined get-type requires a bijection between input length and output length. Since it requires polymorphism we get a reverse get-len via free theorems and both compositions are required to be identities. Thus the case is restricted without providing new insights.
2012-09-27	move definition of get-type to BFF and use it everywhere	Helmut Grohne

2012-06-19	third definition of bff	Helmut Grohne
	It is a definition based on Vec but with less assumptions. The VecBFF has therefore been renamed to VecRevBFF. VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m
2012-06-05	make the Vec bff more similar to the List version	Helmut Grohne

2012-06-05	define a bff over Vec	Helmut Grohne

2012-06-05	move bff and friends to submodule ListBFF	Helmut Grohne