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

Age	Commit message (Collapse)	Author
2013-12-17	update bff implementation to use delete	Helmut Grohne
	In the presence of shape-changing updates, bff needs to shrink one of the mappings before unifying them. As long the shape does not change, the union becomes a disjoint union. With this insight we can adapt the proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately theorem-2 requires more work and assoc-enough becomes non-trivial due to the introduction of mapMV.
2013-07-21	import _>>=_ and fmap from Data.Maybe	Helmut Grohne
	Also rename fmap to _<$>_ to match Agda naming conventions. The imported _>>=_ appears to have different binding, so some braces were necessary.
2013-04-19	move lemma-\notin-lookupM-assoc to Precond	Helmut Grohne
	This removes imports.
2013-04-14	simpler formulation of All-different	Helmut Grohne

2013-01-10	clean imports of Precond	Helmut Grohne

2013-01-10	use different formulation of all-different	Helmut Grohne
	Suggested by Joachim Breitner.
2012-12-14	un-inline different-drop	Helmut Grohne

2012-11-19	we can also drop an implicit parameter from assoc-enough	Helmut Grohne

2012-11-19	we can use one more \exists in assoc-enough	Helmut Grohne

2012-11-19	strip prose from assoc-enough	Helmut Grohne

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-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.