summaryrefslogtreecommitdiff
path: root/FinMap.agda
AgeCommit message (Expand)Author
2022-08-18fix deprecation warning about Any.any with agda-stdlib 1.7.1HEADmasterHelmut Grohne
2020-08-01move imports for agda-stdlib 1.3Helmut Grohne
2020-08-01individually open ≡-ReasoningHelmut Grohne
2019-09-29port to agda/2.6.0.1 and agda-stdlib/1.1Helmut Grohne
2019-03-31Generic.just-injective is Data.Maybe.just-injectiveHelmut Grohne
2019-03-31FinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookupâ...Helmut Grohne
2019-03-31FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulateHelmut Grohne
2019-03-31FinMap.lemma-tabulate-∘ is also known as Data.Vec.Properties.tabulate-congHelmut Grohne
2019-03-31replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicateHelmut Grohne
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut Grohne
2018-11-25remove unused importsHelmut Grohne
2018-11-25reorganize equality importsHelmut Grohne
2018-01-02remove lemma-lookupM-insert-other in favour of lookup∘update′Helmut Grohne
2018-01-02remove lemma-lookupM-insert in favour of lookup∘updateHelmut Grohne
2018-01-01fix compilation with agda 2.5.3, agda-stdlib 0.14Helmut Grohne
2015-07-02split lemma-union-not-used into lemma-exchange-mapsHelmut Grohne
2015-06-03rewrite lemma-disjoint-union in a more compositional wayHelmut Grohne
2014-11-26fix compilation against agda stdlib 0.9Helmut Grohne
2014-10-30make more parameters implicitHelmut Grohne
2014-10-20change restrict and fromAscList to work with VecHelmut Grohne
2014-10-16sym result of lemma-lookupM-{i,checkI}nsert-otherHelmut Grohne
2014-10-15remove lemma-just≢nothingHelmut Grohne
2014-02-26fix compilation on Agda 2.3.0.1Helmut Grohne
2014-02-24define fromFunc more convenientlyHelmut Grohne
2014-02-17fix compilation on Agda 2.3.0.1Helmut Grohne
2014-02-10Merge branch master into feature-shape-updateHelmut Grohne
2014-02-07eliminate useless withsHelmut Grohne
2014-02-07allow shape shape updates in bffHelmut Grohne
2014-02-05add lemma-lookupM-fromFuncHelmut Grohne
2014-02-03make things compile with 2.3.0.1Helmut Grohne
2014-01-28use the indexed version of the Vec SetoidHelmut Grohne
2014-01-27Merge branch feature-deleteHelmut Grohne
2014-01-23show a stronger lemma-checkInsert-restrictHelmut Grohne
2014-01-16generalize lemma-insert-same to arbitrary SetoidsHelmut Grohne
2013-12-17refactor to get rid of FinMap without Maybe entirelyHelmut Grohne
2013-12-17update bff implementation to use deleteHelmut Grohne
2013-12-16move generic functions to a new Generic moduleHelmut Grohne
2013-12-16add new functions delete, delete-many and partializeHelmut Grohne
2013-04-18trim lemma-union-restrictHelmut Grohne
2013-01-28polish lemmata in FinMapHelmut Grohne
2013-01-14define a more useful version of lemma-just\==nnothingHelmut Grohne
2013-01-05shrink lemma-tabulate-\circ using cong\_2Helmut Grohne
2012-12-10get rid of contrapositionHelmut Grohne
2012-11-22shorten line lengths lemma-union-restrictHelmut Grohne
2012-10-25rename lemma-from-just to just-injectiveHelmut Grohne
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
2012-04-27use fromFunc to define unionHelmut Grohne
2012-04-19FinMap: lemma-lookupM-restrict drop useless implicitHelmut Grohne
2012-04-19move lemma-just!=nothing to FinMap and use it thereHelmut Grohne
2012-02-09avoid a sym in lemma-union-restrictHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 06:29:32 +0000