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

Age	Commit message (Collapse)	Author
2014-02-24	define mapMV via sequenceV	Helmut Grohne
	This makes a few proofs easier and eliminates the need for sequence-map entirely.
2014-02-17	Merge branch feature-partial-getlen into master	Helmut Grohne
	It allows defining get functions that are only defined for some vector lengths. It retains backwards compatibility with the previous state via a VecVec compatibility module. The biggest benefit is that now standard library functions such as tail, take and drop can be passed to bff. Conflicts: heavy BFF.agda (imports, bff type clash) Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and lemma-get-mapMV) Generic.agda (imports) Precond.agda (imports, bff type clash in assoc-enough)
2014-02-07	eliminate useless withs	Helmut Grohne

2014-02-07	replace rewrite with cong where feasible	Helmut Grohne

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-30	express VecBFF via PartialVecBFF	Helmut Grohne

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