summaryrefslogtreecommitdiff
path: root/Bidir.agda
AgeCommit message (Expand)Author
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut Grohne
2018-11-25make the setoid parameter to sequenceV-cong explicitHelmut Grohne
2018-11-25reorganize equality importsHelmut Grohne
2018-01-02remove lemma-lookupM-insert in favour of lookup∘updateHelmut Grohne
2016-06-21fix compilation with agda 2.5.1, agda-stdlib 0.12Helmut Grohne
2015-07-02split lemma-union-not-used into lemma-exchange-mapsHelmut Grohne
2015-06-10use "module _" to simplify types involving Get recordsHelmut Grohne
2015-06-09drop barred members from GetTypesHelmut Grohne
2015-01-05SetoidReasoning is no longer neededHelmut Grohne
2014-10-30make more parameters implicitHelmut Grohne
2014-10-21move all those toList calls inside _in-domain-of_Helmut Grohne
2014-10-20change restrict and fromAscList to work with VecHelmut Grohne
2014-10-17generalize lemma-union-not-usedHelmut Grohne
2014-03-10also allow Shaped types for the viewHelmut Grohne
2014-03-10generalize lemma-{just-sequence,sequence-successful}Helmut Grohne
2014-03-10port theorem-{1,2} to PartialShapeVecHelmut Grohne
2014-03-07improve notation of theorem-1 using local bindingsHelmut Grohne
2014-03-07use allFin rather than tabulate idHelmut Grohne
2014-03-05Merge branch feature-omit-sequence into masterHelmut Grohne
2014-03-04make lemma-sequenceV-successful more preciseHelmut Grohne
2014-02-26weaken assumptions made by theorem-2 and asssoc-enoughHelmut Grohne
2014-02-26remove the sequenceV call from bffHelmut Grohne
2014-02-24theorem-2 works with EqR rather than SetoidReasoning againHelmut Grohne
2014-02-24generalize/weaken lemma-get-mapMVHelmut Grohne
2014-02-24define mapMV via sequenceVHelmut Grohne
2014-02-24generalize lemma-lookupM-assocHelmut Grohne
2014-02-21minor simplificationsHelmut Grohne
2014-02-21use map-Σ to simplify lemma-mapM-successfulHelmut Grohne
2014-02-17Merge branch feature-partial-getlen into masterHelmut Grohne
2014-02-17avoid useless repetitionHelmut Grohne
2014-02-10Merge branch master into feature-shape-updateHelmut Grohne
2014-02-07replace rewrite with cong where feasibleHelmut Grohne
2014-02-07allow shape shape updates in bffHelmut Grohne
2014-02-05be more precise about which lookups we useHelmut Grohne
2014-02-05add lemma-lookupM-fromFuncHelmut Grohne
2014-02-04remove unused importsHelmut Grohne
2014-02-04add convenience members to PartialVecVec.GetHelmut Grohne
2014-02-04Merge branch feature-get-record into feature-partial-getlenHelmut Grohne
2014-02-03make things compile with 2.3.0.1Helmut Grohne
2014-01-30fully allow partial get functionsHelmut Grohne
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne
2014-01-30pass get functions as recordsHelmut Grohne
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 18:00:17 +0000