summaryrefslogtreecommitdiff
path: root/Generic.agda
AgeCommit message (Expand)Author
2019-03-31Generic.toList-fromList is Data.Vec.Properties.toList∘fromListHelmut Grohne
2019-03-31Generic.just-injective is Data.Maybe.just-injectiveHelmut Grohne
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut 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
2014-02-24define mapMV via sequenceVHelmut Grohne
2014-02-17Merge branch feature-partial-getlen into masterHelmut Grohne
2014-02-07eliminate useless withsHelmut Grohne
2014-02-07replace rewrite with cong where feasibleHelmut Grohne
2014-02-03make things compile with 2.3.0.1Helmut Grohne
2014-01-30express VecBFF via PartialVecBFFHelmut Grohne
2014-01-28improve readability using _∋_≈_ instead of Setoid._≈_Helmut Grohne
2014-01-28use the indexed version of the Vec SetoidHelmut 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-17show that Vec is an indexed SetoidHelmut Grohne
2014-01-16generalize lemma-insert-same to arbitrary SetoidsHelmut 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 20:25:01 +0000