summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2022-08-18fix deprecation warning about Any.any with agda-stdlib 1.7.1HEADmasterHelmut Grohne
2020-08-01move imports for agda-stdlib 1.3Helmut Grohne
2020-08-01individually open ≡-ReasoningHelmut Grohne
2019-09-29port to agda/2.6.0.1 and agda-stdlib/1.1Helmut Grohne
2019-03-31Generic.toList-fromList is Data.Vec.Properties.toList∘fromListHelmut Grohne
2019-03-31Generic.just-injective is Data.Maybe.just-injectiveHelmut Grohne
2019-03-31FinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookup...Helmut Grohne
2019-03-31FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulateHelmut Grohne
2019-03-31FinMap.lemma-tabulate-∘ is also known as Data.Vec.Properties.tabulate-congHelmut Grohne
2019-03-31replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicateHelmut Grohne
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut Grohne
2018-11-25remove unused importsHelmut Grohne
2018-11-25make the setoid parameter to sequenceV-cong explicitHelmut Grohne
2018-11-25reorganize equality importsHelmut Grohne
2018-11-25fix missing import of "length"Helmut Grohne
2018-01-02length-replicate is now upstream as wellHelmut Grohne
2018-01-02remove lemma-lookupM-insert-other in favour of lookup∘update′Helmut Grohne
2018-01-02remove lemma-lookupM-insert in favour of lookup∘updateHelmut Grohne
2018-01-01fix compilation with agda 2.5.3, agda-stdlib 0.14Helmut Grohne
2016-06-21fix compilation with agda 2.5.1, agda-stdlib 0.12Helmut Grohne
2015-08-11declare copyright and licenseHelmut Grohne
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 02:17:57 +0000