From ee18555869e9c6c61499f12f94f11ce267a0cb85 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Tue, 2 Jan 2024 03:03:13 +0000
Subject: [PATCH] Add `(++)` for `List` variation of `All` (#3179)

* Add `(++)` for `All` for `List`

* changelog

* contributors

* review changes

* update comment

* update comment

* match TODO style

* disambiguate the right one

* further comment changes
---
 CHANGELOG.md                                  | 2 ++
 CONTRIBUTORS                                  | 1 +
 libs/base/Data/List/Quantifiers.idr           | 6 ++++++
 src/Libraries/Data/List/Quantifiers/Extra.idr | 4 +++-
 4 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b3b1e56235..af5252426a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,6 +16,8 @@
 
 * Added an `Interpolation` implementation for primitive decimal numeric types and `Nat`.
 
+* Added append `(++)` for `List` version of `All`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index c6e15d783f..f3ceb93d29 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -33,6 +33,7 @@ Ilya Rezvov
 Jan de Muijnck-Hughes
 Jeetu
 Jens Petersen
+Joel Berkeley
 Joey Eremondi
 Johann Rudloff
 Kamil Shakirov
diff --git a/libs/base/Data/List/Quantifiers.idr b/libs/base/Data/List/Quantifiers.idr
index b0eaf22585..41cde67ba5 100644
--- a/libs/base/Data/List/Quantifiers.idr
+++ b/libs/base/Data/List/Quantifiers.idr
@@ -166,6 +166,12 @@ namespace All
   HList : List Type -> Type
   HList = All id
 
+  ||| Concatenate lists of proofs.
+  public export
+  (++) : All p xs -> All p ys -> All p (xs ++ ys)
+  [] ++ pys = pys
+  (px :: pxs) ++ pys = px :: (pxs ++ pys)
+
   export
   splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)
   splitAt [] pxs = ([], pxs)
diff --git a/src/Libraries/Data/List/Quantifiers/Extra.idr b/src/Libraries/Data/List/Quantifiers/Extra.idr
index e3c8c71df3..8ae595c613 100644
--- a/src/Libraries/Data/List/Quantifiers/Extra.idr
+++ b/src/Libraries/Data/List/Quantifiers/Extra.idr
@@ -14,10 +14,12 @@ lookup v (px :: pxs)
       No _ => lookup v pxs
       Yes Refl => Just px
 
+-- TODO: delete this function after 0.7.1 is released
+-- as it now exists in base's Data.List.Quantifiers
 export
 (++) : All p xs -> All p ys -> All p (xs ++ ys)
 [] ++ pys = pys
-(px :: pxs) ++ pys = px :: (pxs ++ pys)
+(px :: pxs) ++ pys = px :: (Extra.(++) pxs pys)
 
 export
 tabulate : ((x : a) -> p x) -> (xs : List a) -> All p xs