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

Age	Commit message (Collapse)	Author
2014-02-03	make things compile with 2.3.0.1	Helmut Grohne
	* Remove let patter , match = foo usage * Remove Qualified.infix-symbol usage * Add non-obvious absurd patterns * Qualify constructors
2014-01-28	improve readability using _∋_≈_ instead of Setoid._≈_	Helmut Grohne

2014-01-28	use the indexed version of the Vec Setoid	Helmut Grohne

2014-01-27	Merge branch feature-delete	Helmut Grohne
	Most conflicts stem from varying imports or added functions and a take-both approach merges them. A notable exception is theorem-2, where a new result sequence-cong was required. Apart from that, theorem-2 could be taken almost verbatim from feature-delete albeit its type coming from feature-decsetoid. Conflicts: Bidir.agda FinMap.agda Generic.agda Precond.agda
2014-01-27	cleanup unused functions and useless steps	Helmut Grohne

2014-01-24	prove theorem-2 in the presence of delete	Helmut Grohne
	The biggest piece of this puzzle was establishing get <$> mapMV f v == mapMV f (get v) provided that the result of mapMV is just something. lemma-union-not-used lost a "map just", but could be retained in structure.
2014-01-17	show that Vec is an indexed Setoid	Helmut Grohne
	We get the plain Setoid for free then.
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	add a mapM variant on the Maybe monad on Vecs	Helmut Grohne

2013-12-16	move generic functions to a new Generic module	Helmut Grohne