summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-26weaken assumptions made by theorem-2 and asssoc-enoughHelmut Grohne
2014-02-26remove the sequenceV call from bffHelmut Grohne
2014-02-26fix compilation on Agda 2.3.0.1Helmut Grohne
2014-02-26convert LiftGet module to using heterogeneous equalityHelmut Grohne
2014-02-24add intersperse as another exampleHelmut Grohne
2014-02-24theorem-2 works with EqR rather than SetoidReasoning againHelmut Grohne
2014-02-24define fromFunc more convenientlyHelmut 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-17fix compilation on Agda 2.3.0.1Helmut Grohne
2014-02-17use drop, tail and take from Data.Vec in examplesHelmut Grohne
2014-02-17switch examples to PartialVecVecHelmut Grohne
2014-02-17Merge branch feature-partial-getlen into masterHelmut Grohne
2014-02-17avoid useless repetitionHelmut Grohne
2014-02-14Merge branch feature-shape-update into masterHelmut Grohne
2014-02-14add back original bff function before shape updatesHelmut Grohne
2014-02-10add bffplug and bffinv functions and examplesHelmut Grohne
2014-02-10Merge branch master into feature-shape-updateHelmut Grohne
2014-02-10add sieve to examplesHelmut Grohne
2014-02-07eliminate useless withsHelmut 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-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-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-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-30fully allow partial get functionsHelmut Grohne
2014-01-30make the getlen functions explicit in PartialVecBFFHelmut Grohne
2014-01-30express VecBFF via PartialVecBFFHelmut 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-28define bff on a partial getlenHelmut 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 23:24:48 +0000