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

Age	Commit message (Collapse)	Author
2013-12-17	refactor to get rid of FinMap without Maybe entirely	Helmut Grohne
	The union was the only user of this type and now it uses only partial mappings. So drop remaining uses of FinMap and make everything work with FinMapMaybe instead.
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-12-16	move generic functions to a new Generic module	Helmut Grohne

2013-12-16	add new functions delete, delete-many and partialize	Helmut Grohne
	and accompanying lemmata.
2013-04-18	trim lemma-union-restrict	Helmut Grohne

2013-01-28	polish lemmata in FinMap	Helmut Grohne

2013-01-14	define a more useful version of lemma-just\==nnothing	Helmut Grohne
	If one had a parameter of type just x \== nothing it could be simply refuted by case splitting. So the cases where lemma-just\==nnothing was used always employed trans to combine two results. The new version takes both results instead.
2013-01-05	shrink lemma-tabulate-\circ using cong\_2	Helmut Grohne

2012-12-10	get rid of contraposition	Helmut Grohne
	Using function composition in all other places already.
2012-11-22	shorten line lengths lemma-union-restrict	Helmut Grohne

2012-10-25	rename lemma-from-just to just-injective	Helmut Grohne
	We already have suc-injective and \::-injective. Consistency!
2012-09-26	use _\==n_ and _\notin_ instead of \neg	Helmut Grohne
	Consistent. Shorter.
2012-04-27	use fromFunc to define union	Helmut Grohne
	Semantically this is no change, but reducing to standard interface seems better.
2012-04-19	FinMap: lemma-lookupM-restrict drop useless implicit	Helmut Grohne

2012-04-19	move lemma-just!=nothing to FinMap and use it there	Helmut Grohne

2012-02-09	avoid a sym in lemma-union-restrict	Helmut Grohne

2012-02-09	s/generate/restrict/g	Helmut Grohne
	The name was deemed misleading. Nothing else changed.
2012-02-09	prove lemma-union-generate	Helmut Grohne

2012-01-26	split Bidir.agda to FinMap.agda	Helmut Grohne