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
idris-lang · Jan 2, 2024 · ee18555 · ee18555
1 parent 7815f20
commit ee18555
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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
@@ -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