[ new ] updateAt and extra Properties on List.All

CHANGELOG.md

@@ -161,6 +161,13 @@ Other minor additions
   mapM      : (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
   forA      : All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
   forM      : All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
+
+  _++_      : ∀ {l m} → All P l → All P m → All P (l List.++ m)
+  _∷ʳ_      : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
+
+  updateAt  : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
+  _[_]%=_   : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
+  _[_]≔_    : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
   ```
 
 * Added new operators to `Data.List.Base`:

src/Data/List/All.agda

@@ -54,6 +54,34 @@ map : ∀ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} →
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
+------------------------------------------------------------------------
+-- concat and append
+
+module _ {a p}{A : Set a}{P : Pred A p} where
+
+  _++_ : ∀ {l m} → All P l → All P m → All P (l List.++ m)
+  [] ++ pm = pm
+  (px ∷ pl) ++ pm = px ∷ (pl ++ pm)
+
+  _∷ʳ_ : ∀ {l : List A}{x} → All P l → P x → All P (l List.∷ʳ x)
+  pxs ∷ʳ px = pxs ++ (px ∷ [])
+
+------------------------------------------------------------------------
+-- (weak) updateAt
+module _ {a p}{A : Set a}{P : Pred A p} where
+  infixl 6 _[_]%=_ _[_]≔_
+
+  updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
+  updateAt () f []
+  updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
+  updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs
+
+  _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
+  pxs [ i ]%= f = updateAt i f pxs
+
+  _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
+  pxs [ i ]≔ px = pxs [ i ]%= const px
+
 ------------------------------------------------------------------------
 -- (un/)zip(With/)