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

Age	Commit message (Collapse)	Author
2014-01-16	generalize lemma-insert-same to arbitrary Setoids	Helmut Grohne
	The general idea is to enable bff to use arbitrary DecSetoids. * assoc needs to learn about DecSetoid * checkInsert needs to learn about DecSetoid * InsertionResult needs to learn about Setoid * Parameters to InsertionResult.same become weaker * lemma-checkInsert-restrict should work with weaker same * lemma-insert-same needs to learn about Setoid
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