sym result of lemma-lookupM-{i,checkI}nsert-other
[~helmut/bidiragda.git] / Generic.agda
2014-02-24 Helmut Grohnedefine mapMV via sequenceV
2014-02-17 Helmut GrohneMerge branch feature-partial-getlen into master
2014-02-10 Helmut GrohneMerge branch master into feature-shape-update
2014-02-07 Helmut Grohneeliminate useless withs
2014-02-07 Helmut Grohnereplace rewrite with cong where feasible
2014-02-04 Helmut GrohneMerge branch feature-get-record into feature-partial...
2014-02-03 Helmut Grohnemake things compile with 2.3.0.1
2014-01-30 Helmut Grohneexpress VecBFF via PartialVecBFF
2014-01-28 Helmut Grohneimprove readability using _∋_≈_ instead of Setoid._≈_
2014-01-28 Helmut Grohneuse the indexed version of the Vec Setoid
2014-01-27 Helmut GrohneMerge branch feature-delete
2014-01-27 Helmut GrohneMerge branch feature-decsetoid
2014-01-27 Helmut Grohnecleanup unused functions and useless steps
2014-01-24 Helmut Grohneprove theorem-2 in the presence of delete
2014-01-17 Helmut Grohneshow that Vec is an indexed Setoid
2014-01-16 Helmut Grohnegeneralize lemma-insert-same to arbitrary Setoids
2013-12-16 Helmut Grohneadd a mapM variant on the Maybe monad on Vecs
2013-12-16 Helmut Grohnemove generic functions to a new Generic module