move imports for agda-stdlib 1.3
[~helmut/bidiragda.git] / FinMap.agda
2020-08-01 Helmut Grohnemove imports for agda-stdlib 1.3 master
2020-08-01 Helmut Grohneindividually open ≡-Reasoning
2019-09-29 Helmut Grohneport to agda/2.6.0.1 and agda-stdlib/1.1
2019-03-31 Helmut GrohneGeneric.just-injective is Data.Maybe.just-injective
2019-03-31 Helmut GrohneFinMap.lemma-lookupM-delete is another variant of Data...
2019-03-31 Helmut GrohneFinMap.lemma-lookupM-fromFunc is almost Data.Vec.Proper...
2019-03-31 Helmut GrohneFinMap.lemma-tabulate-∘ is also known as Data.Vec.Prope...
2019-03-31 Helmut Grohnereplace FinMap.lemma-lookupM-empty with Data.Vec.Proper...
2018-11-25 Helmut Grohneport to agda/2.5.4.1 and agda-stdlib/0.17
2018-11-25 Helmut Grohneremove unused imports
2018-11-25 Helmut Grohnereorganize equality imports
2018-01-02 Helmut Grohneremove lemma-lookupM-insert-other in favour of lookup...
2018-01-02 Helmut Grohneremove lemma-lookupM-insert in favour of lookup∘update
2018-01-01 Helmut Grohnefix compilation with agda 2.5.3, agda-stdlib 0.14
2015-07-02 Helmut Grohnesplit lemma-union-not-used into lemma-exchange-maps
2015-06-03 Helmut Grohnerewrite lemma-disjoint-union in a more compositional way
2014-11-26 Helmut Grohnefix compilation against agda stdlib 0.9
2014-10-30 Helmut Grohnemake more parameters implicit
2014-10-20 Helmut Grohnechange restrict and fromAscList to work with Vec
2014-10-16 Helmut Grohnesym result of lemma-lookupM-{i,checkI}nsert-other
2014-10-15 Helmut Grohneremove lemma-just≢nothing
2014-02-26 Helmut Grohnefix compilation on Agda 2.3.0.1
2014-02-24 Helmut Grohnedefine fromFunc more conveniently
2014-02-17 Helmut Grohnefix compilation on Agda 2.3.0.1
2014-02-17 Helmut GrohneMerge branch feature-partial-getlen into master
2014-02-14 Helmut GrohneMerge branch feature-shape-update into master
2014-02-10 Helmut GrohneMerge branch master into feature-shape-update
2014-02-07 Helmut Grohneeliminate useless withs
2014-02-07 Helmut Grohneallow shape shape updates in bff
2014-02-05 Helmut Grohneadd lemma-lookupM-fromFunc
2014-02-03 Helmut Grohnemake things compile with 2.3.0.1
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-23 Helmut Grohneshow a stronger lemma-checkInsert-restrict
2014-01-16 Helmut Grohnegeneralize lemma-insert-same to arbitrary Setoids
2013-12-17 Helmut Grohnerefactor to get rid of FinMap without Maybe entirely
2013-12-17 Helmut Grohneupdate bff implementation to use delete
2013-12-16 Helmut Grohnemove generic functions to a new Generic module
2013-12-16 Helmut Grohneadd new functions delete, delete-many and partialize
2013-04-18 Helmut Grohnetrim lemma-union-restrict
2013-01-28 Helmut Grohnepolish lemmata in FinMap
2013-01-17 Helmut GrohneMerge branch view2 into master
2013-01-14 Helmut Grohnedefine a more useful version of lemma-just\==nnothing
2013-01-05 Helmut Grohneshrink lemma-tabulate-\circ using cong\_2
2012-12-10 Helmut Grohneget rid of contraposition
2012-11-22 Helmut Grohneshorten line lengths lemma-union-restrict
2012-10-25 Helmut Grohnerename lemma-from-just to just-injective
2012-09-26 Helmut Grohneuse _\==n_ and _\notin_ instead of \neg
2012-04-27 Helmut Grohneuse fromFunc to define union
2012-04-19 Helmut GrohneFinMap: lemma-lookupM-restrict drop useless implicit
2012-04-19 Helmut Grohnemove lemma-just!=nothing to FinMap and use it there
2012-02-09 Helmut Grohneavoid a sym in lemma-union-restrict
2012-02-09 Helmut Grohnes/generate/restrict/g
2012-02-09 Helmut Grohneprove lemma-union-generate
2012-01-26 Helmut Grohnesplit Bidir.agda to FinMap.agda