summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-07eliminate useless withsHelmut Grohne
2014-02-07replace rewrite with cong where feasibleHelmut Grohne
2014-02-05be more precise about which lookups we useHelmut Grohne
2014-02-05strip even more implementation detail in PrecondHelmut Grohne
2014-02-05strip implementation detail from lemma-union-delete-fromFuncHelmut Grohne
2014-02-05add lemma-lookupM-fromFuncHelmut Grohne
2014-02-05add examplesHelmut Grohne
2014-02-03make things compile with 2.3.0.1Helmut Grohne
2014-02-03Merge branch feature-get-record into masterHelmut Grohne
2014-02-03also show the other direction GetL-to-GetVHelmut Grohne
2014-02-03add a GetV-to-GetL transformerHelmut Grohne
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne
2014-01-30pass get functions as recordsHelmut Grohne
2014-01-30simplify compilation of the whole sourceHelmut Grohne
2014-01-28improve readability using _∋_≈_ instead of Setoid._≈_Helmut Grohne
2014-01-28there is no need to work with IsPreorderHelmut 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-27Merge branch feature-decsetoidHelmut Grohne
2014-01-27cleanup unused functions and useless stepsHelmut Grohne
2014-01-27prove assoc-enough in the presence of deleteHelmut 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
2014-01-17show that Vec is an indexed SetoidHelmut 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-16add a mapM variant on the Maybe monad on VecsHelmut Grohne
2013-12-16move generic functions to a new Generic moduleHelmut Grohne
2013-12-16add new functions delete, delete-many and partializeHelmut Grohne
2013-12-16get rid of the ListBFF implementationHelmut 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-18trim lemma-union-restrictHelmut Grohne
2013-04-14simpler formulation of All-differentHelmut Grohne
2013-04-10lemma-map-lookupM-assoc is even simplerHelmut Grohne
2013-04-09rewrite lemma-map-lookupM-assocHelmut Grohne
2013-02-01employ insertionresult in lemma-lookupM-checkInsertHelmut Grohne
2013-01-28drop the insert- prefix from the insertionresult ctorsHelmut Grohne
2013-01-28polish lemmata in FinMapHelmut 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-10clean imports of PrecondHelmut Grohne
2013-01-10use different formulation of all-differentHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-02 05:37:37 +0000