summaryrefslogtreecommitdiff
path: root/Bidir.agda
AgeCommit message (Expand)Author
2014-01-28improve readability using _∋_≈_ instead of Setoid._≈_Helmut Grohne
2014-01-28use the indexed version of the Vec SetoidHelmut Grohne
2014-01-28cleanup unused function and importHelmut Grohne
2014-01-27Merge branch feature-deleteHelmut Grohne
2014-01-27cleanup unused functions and useless stepsHelmut Grohne
2014-01-24prove theorem-2 in the presence of deleteHelmut Grohne
2014-01-23generalize BFF and theorem-2 to arbitrary SetoidsHelmut Grohne
2014-01-23show a stronger lemma-checkInsert-restrictHelmut Grohne
2014-01-17generalize checkInsert 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-10-02need to fully qualify Data.List.All._::_Helmut Grohne
2013-07-21import _>>=_ and fmap from Data.MaybeHelmut Grohne
2013-04-19move lemma-\notin-lookupM-assoc to PrecondHelmut Grohne
2013-04-10lemma-map-lookupM-assoc is even simplerHelmut Grohne
2013-04-09rewrite lemma-map-lookupM-assocHelmut Grohne
2013-01-28drop the insert- prefix from the insertionresult ctorsHelmut Grohne
2013-01-17Merge branch view2 into masterHelmut Grohne
2013-01-14shrink lemma-union-not-used by matching on All's ctorHelmut Grohne
2013-01-14define a more useful version of lemma-just\==nnothingHelmut Grohne
2013-01-12introduce a proper view on checkInsertHelmut Grohne
2013-01-10reduce a precondition of lemma-checkInsert-lookupMHelmut Grohne
2013-01-10rewrite lemma-\notin-lookupM-assocHelmut Grohne
2013-01-05shrink lemma-union-not-used using cong\_2Helmut Grohne
2013-01-05shrink lemma-map-lookupM-insert using cong\_2Helmut Grohne
2013-01-05shrink base case of lemma-/notin-lookupM-assocHelmut Grohne
2012-12-10drop unused importHelmut Grohne
2012-12-10drop unused param from lemma-map-lookupM-insertHelmut Grohne
2012-12-07reduce useless case in lemma-map-lookupM-assocHelmut Grohne
2012-11-22shorten line lengths of theorem-2Helmut Grohne
2012-11-22shorten line length of theorem-1Helmut Grohne
2012-11-19turn lemma-fmap-just parameter into implicitHelmut Grohne
2012-11-17strip prose from lemma-1 and lemma-2Helmut Grohne
2012-10-25similarly rename lemma-from-map-just to map-just-injectiveHelmut Grohne
2012-10-25rename lemma-from-just to just-injectiveHelmut Grohne
2012-10-22finally parameterize CheckInsertHelmut Grohne
2012-10-22now parameterize BFFHelmut Grohne
2012-10-22parameterize Bidir via Carrier and deqHelmut Grohne
2012-10-05move all postulates to one moduleHelmut Grohne
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
2012-09-26import [_] instead of Reveal_is_Helmut Grohne
2012-09-18Merge branch 'using-vec'Helmut Grohne
2012-09-17save a with in lemma-\inn-lookupM-assocHelmut Grohne
2012-09-14employ rewrite in lemma-map-lookupM-assocHelmut Grohne
2012-09-04rewrite main theorems to using Vec instead of ListHelmut Grohne
2012-06-05move bff and friends to submodule ListBFFHelmut Grohne
2012-06-05move checkInsert and related properties to CheckInsert.agdaHelmut Grohne
2012-04-27lemma-2: do not confuse lookup with lookupMHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 23:21:08 +0000