summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-02split lemma-union-not-used into lemma-exchange-mapsHelmut Grohne
2015-06-12add example applications of bffHelmut Grohne
2015-06-10use "module _" to simplify types involving Get recordsHelmut Grohne
2015-06-09drop barred members from GetTypesHelmut Grohne
2015-06-09drop the Function.Equality requirement from GetTypesHelmut Grohne
2015-06-03rewrite lemma-disjoint-union in a more compositional wayHelmut Grohne
2015-01-05SetoidReasoning is no longer neededHelmut Grohne
2015-01-05turns out: ind-cong is a special case of H.cong₂Helmut Grohne
2014-11-26fix compilation against agda stdlib 0.9Helmut 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-10-16sym result of lemma-lookupM-{i,checkI}nsert-otherHelmut Grohne
2014-10-15remove lemma-just≢nothingHelmut Grohne
2014-10-14drop the injection requirement for gl₁Helmut Grohne
2014-09-26resolve ambiguity in BFFPlugHelmut Grohne
2014-06-06drop-suc is cong predHelmut Grohne
2014-04-03fix compilation for Agda 2.3.0.1 againHelmut Grohne
2014-04-03Merge branch feature-shaped into masterHelmut Grohne
2014-04-03drop PartialShapeVecHelmut Grohne
2014-03-10also allow Shaped types for the viewHelmut Grohne
2014-03-10generalize lemma-{just-sequence,sequence-successful}Helmut Grohne
2014-03-10Example: show that PairVec is ShapedHelmut Grohne
2014-03-10port precondition to PartialShapeVecHelmut Grohne
2014-03-10port theorem-{1,2} to PartialShapeVecHelmut Grohne
2014-03-10implement a bff on a shaped source typeHelmut Grohne
2014-03-07add a Functor structureHelmut 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-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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 23:28:53 +0000