From 1b1ef447b8d2d3ecf494a6bf607dc8c2e6ecf7a6 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Sun, 13 Aug 2023 17:00:28 -0400 Subject: [PATCH 1/5] improve implementation of splitAt, take and drop. Seriously simplifies various proofs. --- src/Data/Vec/Base.agda | 11 ++++------- src/Data/Vec/Properties.agda | 8 ++------ src/Data/Vec/Relation/Unary/All/Properties.agda | 6 ++---- src/Data/Vec/Relation/Unary/AllPairs/Properties.agda | 6 ++---- 4 files changed, 10 insertions(+), 21 deletions(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 9f6d86b792..4ea50e4eb2 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool; true; false; if_then_else_) open import Data.Nat.Base open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List) -open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_) +open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂) open import Data.These.Base as These using (These; this; that; these) open import Function.Base using (const; _∘′_; id; _∘_) open import Level using (Level) @@ -263,16 +263,13 @@ splitAt : ∀ m {n} (xs : Vec A (m + n)) → ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs splitAt zero xs = ([] , xs , refl) splitAt (suc m) (x ∷ xs) with splitAt m xs -splitAt (suc m) (x ∷ .(ys ++ zs)) | (ys , zs , refl) = - ((x ∷ ys) , zs , refl) +splitAt (suc m) (x ∷ xs) | (ys , zs , p) = ((x ∷ ys) , zs , cong (x ∷_) p) take : ∀ m {n} → Vec A (m + n) → Vec A m -take m xs with splitAt m xs -take m .(ys ++ zs) | (ys , zs , refl) = ys +take m xs = proj₁ (splitAt m xs) drop : ∀ m {n} → Vec A (m + n) → Vec A n -drop m xs with splitAt m xs -drop m .(ys ++ zs) | (ys , zs , refl) = zs +drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 49924a7b31..fdf5272be2 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -215,12 +215,8 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) → lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i -lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs) - rewrite unfold-take m x xs = refl -lookup-inject≤-take (suc (suc m)) (s≤s m≤m+n) (suc zero) (x ∷ y ∷ xs) - rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = refl -lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ y ∷ xs) - rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = lookup-inject≤-take m m≤m+n i xs +lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs) = refl +lookup-inject≤-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-inject≤-take m m≤m+n i xs ------------------------------------------------------------------------ -- updateAt (_[_]%=_) diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 868620ff74..9cfc066635 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -148,13 +148,11 @@ module _ {P : A → Set p} where drop⁺ : ∀ m {xs} → All P {m + n} xs → All P {n} (drop m xs) drop⁺ zero pxs = pxs -drop⁺ (suc m) {x ∷ xs} (px ∷ pxs) - rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs +drop⁺ (suc m) {x ∷ xs} (px ∷ pxs) = drop⁺ m pxs take⁺ : ∀ m {xs} → All P {m + n} xs → All P {m} (take m xs) take⁺ zero pxs = [] -take⁺ (suc m) {x ∷ xs} (px ∷ pxs) - rewrite Vecₚ.unfold-take m x xs = px ∷ take⁺ m pxs +take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = px ∷ take⁺ m pxs ------------------------------------------------------------------------ -- toList diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index 2158246fbc..81cdff0706 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -70,13 +70,11 @@ module _ {R : Rel A ℓ} where take⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {m} (take m xs) take⁺ zero pxs = [] - take⁺ (suc m) {x ∷ xs} (px ∷ pxs) - rewrite Vecₚ.unfold-take m x xs = Allₚ.take⁺ m px ∷ take⁺ m pxs + take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = Allₚ.take⁺ m px ∷ take⁺ m pxs drop⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {n} (drop m xs) drop⁺ zero pxs = pxs - drop⁺ (suc m) {x ∷ xs} (_ ∷ pxs) - rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs + drop⁺ (suc m) {x ∷ xs} (_ ∷ pxs) = drop⁺ m pxs ------------------------------------------------------------------------ -- tabulate From 8920a12a0220d3093cec2038e27d7168b3d0f54b Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 14 Aug 2023 22:21:49 -0400 Subject: [PATCH 2/5] Remove some additional with calls that were not needed. Fix a number of proofs to no longer need unfold-take nor unfold-drop (and these are now trivial as well). Simplify group somewhat as well. --- src/Data/Vec/Base.agda | 21 ++++++------- src/Data/Vec/Properties.agda | 57 +++++------------------------------- 2 files changed, 16 insertions(+), 62 deletions(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 4ea50e4eb2..d8397d038d 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -16,7 +16,7 @@ open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; pr open import Data.These.Base as These using (These; this; that; these) open import Function.Base using (const; _∘′_; id; _∘_) open import Level using (Level) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong) open import Relation.Nullary.Decidable.Core using (does) open import Relation.Unary using (Pred; Decidable) @@ -262,8 +262,8 @@ allFin _ = tabulate id splitAt : ∀ m {n} (xs : Vec A (m + n)) → ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs splitAt zero xs = ([] , xs , refl) -splitAt (suc m) (x ∷ xs) with splitAt m xs -splitAt (suc m) (x ∷ xs) | (ys , zs , p) = ((x ∷ ys) , zs , cong (x ∷_) p) +splitAt (suc m) (x ∷ xs) = + let (ys , zs , eq) = splitAt m xs in ((x ∷ ys) , zs , cong (x ∷_) eq) take : ∀ m {n} → Vec A (m + n) → Vec A m take m xs = proj₁ (splitAt m xs) @@ -274,10 +274,9 @@ drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) -group (suc n) k xs with splitAt k xs -group (suc n) k .(ys ++ zs) | (ys , zs , refl) with group n k zs -group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) = - ((ys ∷ zss) , refl) +group (suc n) k xs with splitAt k xs +group (suc n) k xs | (ys , zs , eq) with group n k zs +group (suc n) k xs | (ys , ._ , eq) | (zss , eq′) = ((ys ∷ zss) , trans eq (cong (ys ++_) eq′)) split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋ split [] = ([] , []) @@ -339,15 +338,13 @@ xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y initLast {n = zero} (x ∷ []) = ([] , x , refl) initLast {n = suc n} (x ∷ xs) with initLast xs -... | (ys , y , refl) = (x ∷ ys , y , refl) +... | (ys , y , eq) = (x ∷ ys , y , cong (x ∷_) eq) init : Vec A (1 + n) → Vec A n -init xs with initLast xs -... | (ys , y , refl) = ys +init xs = proj₁ (initLast xs) last : Vec A (1 + n) → A -last xs with initLast xs -... | (ys , y , refl) = y +last xs = proj₁ (proj₂ (initLast xs)) ------------------------------------------------------------------------ -- Other operations diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index fdf5272be2..7031e200a8 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -71,86 +71,43 @@ private -- take unfold-take : ∀ n x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs -unfold-take n x xs with splitAt n xs -... | xs , ys , refl = refl +unfold-take n x xs = refl take-distr-zipWith : ∀ (f : A → B → C) → (xs : Vec A (m + n)) (ys : Vec B (m + n)) → take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys) take-distr-zipWith {m = zero} f xs ys = refl -take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin - take (suc m) (zipWith f (x ∷ xs) (y ∷ ys)) - ≡⟨⟩ - take (suc m) (f x y ∷ (zipWith f xs ys)) - ≡⟨ unfold-take m (f x y) (zipWith f xs ys) ⟩ - f x y ∷ take m (zipWith f xs ys) - ≡⟨ cong (f x y ∷_) (take-distr-zipWith f xs ys) ⟩ - f x y ∷ (zipWith f (take m xs) (take m ys)) - ≡⟨⟩ - zipWith f (x ∷ (take m xs)) (y ∷ (take m ys)) - ≡˘⟨ cong₂ (zipWith f) (unfold-take m x xs) (unfold-take m y ys) ⟩ - zipWith f (take (suc m) (x ∷ xs)) (take (suc m) (y ∷ ys)) - ∎ +take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (take-distr-zipWith f xs ys) take-distr-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) → take m (map f xs) ≡ map f (take m xs) take-distr-map f zero xs = refl -take-distr-map f (suc m) (x ∷ xs) = begin - take (suc m) (map f (x ∷ xs)) ≡⟨⟩ - take (suc m) (f x ∷ map f xs) ≡⟨ unfold-take m (f x) (map f xs) ⟩ - f x ∷ (take m (map f xs)) ≡⟨ cong (f x ∷_) (take-distr-map f m xs) ⟩ - f x ∷ (map f (take m xs)) ≡⟨⟩ - map f (x ∷ take m xs) ≡˘⟨ cong (map f) (unfold-take m x xs) ⟩ - map f (take (suc m) (x ∷ xs)) ∎ +take-distr-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-distr-map f m xs) ------------------------------------------------------------------------ -- drop unfold-drop : ∀ n x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs -unfold-drop n x xs with splitAt n xs -... | xs , ys , refl = refl +unfold-drop n x xs = refl drop-distr-zipWith : (f : A → B → C) → (x : Vec A (m + n)) (y : Vec B (m + n)) → drop m (zipWith f x y) ≡ zipWith f (drop m x) (drop m y) drop-distr-zipWith {m = zero} f xs ys = refl -drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin - drop (suc m) (zipWith f (x ∷ xs) (y ∷ ys)) - ≡⟨⟩ - drop (suc m) (f x y ∷ (zipWith f xs ys)) - ≡⟨ unfold-drop m (f x y) (zipWith f xs ys) ⟩ - drop m (zipWith f xs ys) - ≡⟨ drop-distr-zipWith f xs ys ⟩ - zipWith f (drop m xs) (drop m ys) - ≡˘⟨ cong₂ (zipWith f) (unfold-drop m x xs) (unfold-drop m y ys) ⟩ - zipWith f (drop (suc m) (x ∷ xs)) (drop (suc m) (y ∷ ys)) - ∎ +drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = drop-distr-zipWith f xs ys drop-distr-map : ∀ (f : A → B) (m : ℕ) (x : Vec A (m + n)) → drop m (map f x) ≡ map f (drop m x) drop-distr-map f zero x = refl -drop-distr-map f (suc m) (x ∷ xs) = begin - drop (suc m) (map f (x ∷ xs)) ≡⟨⟩ - drop (suc m) (f x ∷ map f xs) ≡⟨ unfold-drop m (f x) (map f xs) ⟩ - drop m (map f xs) ≡⟨ drop-distr-map f m xs ⟩ - map f (drop m xs) ≡˘⟨ cong (map f) (unfold-drop m x xs) ⟩ - map f (drop (suc m) (x ∷ xs)) ∎ +drop-distr-map f (suc m) (x ∷ xs) = drop-distr-map f m xs ------------------------------------------------------------------------ -- take and drop together take-drop-id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x take-drop-id zero x = refl -take-drop-id (suc m) (x ∷ xs) = begin - take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs) - ≡⟨ cong₂ _++_ (unfold-take m x xs) (unfold-drop m x xs) ⟩ - (x ∷ take m xs) ++ (drop m xs) - ≡⟨⟩ - x ∷ (take m xs ++ drop m xs) - ≡⟨ cong (x ∷_) (take-drop-id m xs) ⟩ - x ∷ xs - ∎ +take-drop-id (suc m) (x ∷ xs) = cong (x ∷_) (take-drop-id m xs) ------------------------------------------------------------------------ -- truncate From 3041c0a748e762fbab3645075bd3a0a6f059b146 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 16 Aug 2023 10:51:26 -0400 Subject: [PATCH 3/5] implement some of the improvements suggested by @jamesmckinna --- src/Data/Vec/Base.agda | 12 +++++++----- src/Data/Vec/Relation/Unary/AllPairs/Properties.agda | 2 +- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index d8397d038d..d63ea7976e 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -274,9 +274,10 @@ drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) -group (suc n) k xs with splitAt k xs -group (suc n) k xs | (ys , zs , eq) with group n k zs -group (suc n) k xs | (ys , ._ , eq) | (zss , eq′) = ((ys ∷ zss) , trans eq (cong (ys ++_) eq′)) +group (suc n) k xs = + let ys , zs , eq-split = splitAt k xs in + let zss , eq-group = group n k zs in + (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group) split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋ split [] = ([] , []) @@ -337,8 +338,9 @@ xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y initLast {n = zero} (x ∷ []) = ([] , x , refl) -initLast {n = suc n} (x ∷ xs) with initLast xs -... | (ys , y , eq) = (x ∷ ys , y , cong (x ∷_) eq) +initLast {n = suc n} (x ∷ xs) = + let ys , y , eq = initLast xs in + (x ∷ ys , y , cong (x ∷_) eq) init : Vec A (1 + n) → Vec A n init xs = proj₁ (initLast xs) diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index 81cdff0706..ffc0ec6c4c 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -74,7 +74,7 @@ module _ {R : Rel A ℓ} where drop⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {n} (drop m xs) drop⁺ zero pxs = pxs - drop⁺ (suc m) {x ∷ xs} (_ ∷ pxs) = drop⁺ m pxs + drop⁺ (suc m) (_ ∷ pxs) = drop⁺ m pxs ------------------------------------------------------------------------ -- tabulate From 7c136ad05d826c8f6b168a18c5f52e63aeb9b32f Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 13 Sep 2023 16:15:42 +0100 Subject: [PATCH 4/5] Update Properties.agda: renamings and deprecations --- src/Data/Vec/Properties.agda | 57 ++++++++++++++++++++++++------------ 1 file changed, 39 insertions(+), 18 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 15aa47fe72..373f03fe48 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -73,16 +73,16 @@ private unfold-take : ∀ n x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs unfold-take n x xs = refl -take-distr-zipWith : ∀ (f : A → B → C) → - (xs : Vec A (m + n)) (ys : Vec B (m + n)) → - take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys) -take-distr-zipWith {m = zero} f xs ys = refl -take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (take-distr-zipWith f xs ys) +take-zipWith : ∀ (f : A → B → C) → + (xs : Vec A (m + n)) (ys : Vec B (m + n)) → + take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys) +take-zipWith {m = zero} f xs ys = refl +take-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (take-zipWith f xs ys) -take-distr-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) → - take m (map f xs) ≡ map f (take m xs) -take-distr-map f zero xs = refl -take-distr-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-distr-map f m xs) +take-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) → + take m (map f xs) ≡ map f (take m xs) +take-map f zero xs = refl +take-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-map f m xs) ------------------------------------------------------------------------ -- drop @@ -91,16 +91,16 @@ unfold-drop : ∀ n x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs unfold-drop n x xs = refl -drop-distr-zipWith : (f : A → B → C) → - (x : Vec A (m + n)) (y : Vec B (m + n)) → - drop m (zipWith f x y) ≡ zipWith f (drop m x) (drop m y) -drop-distr-zipWith {m = zero} f xs ys = refl -drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = drop-distr-zipWith f xs ys +drop-zipWith : (f : A → B → C) → + (xs : Vec A (m + n)) (ys : Vec B (m + n)) → + drop m (zipWith f xs ys) ≡ zipWith f (drop m xs) (drop m ys) +drop-zipWith {m = zero} f xs ys = refl +drop-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = drop-zipWith f xs ys -drop-distr-map : ∀ (f : A → B) (m : ℕ) (x : Vec A (m + n)) → - drop m (map f x) ≡ map f (drop m x) -drop-distr-map f zero x = refl -drop-distr-map f (suc m) (x ∷ xs) = drop-distr-map f m xs +drop-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) → + drop m (map f xs) ≡ map f (drop m xs) +drop-map f zero xs = refl +drop-map f (suc m) (x ∷ xs) = drop-map f m xs ------------------------------------------------------------------------ -- take and drop together @@ -1176,3 +1176,24 @@ take-drop-id = take++drop≡id "Warning: take-drop-id was deprecated in v2.0. Please use take++drop≡id instead." #-} + +take-distr-zipWith = take-zipWith +{-# WARNING_ON_USAGE take-distr-zipWith +"Warning: take-distr-zipWith was deprecated in v2.0. +Please use take-zipWith instead." +#-} +take-distr-map = take-map +{-# WARNING_ON_USAGE take-distr-map +"Warning: take-distr-map was deprecated in v2.0. +Please use take-map instead." +#-} +drop-distr-zipWith = drop-zipWith +{-# WARNING_ON_USAGE drop-distr-zipWith +"Warning: drop-distr-zipWith was deprecated in v2.0. +Please use tdrop-zipWith instead." +#-} +drop-distr-map = drop-map +{-# WARNING_ON_USAGE drop-distr-map +"Warning: drop-distr-map was deprecated in v2.0. +Please use drop-map instead." +#-} From 2041d3eb56c1f05df97f720c4e42091926060d3e Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 13 Sep 2023 17:27:18 +0100 Subject: [PATCH 5/5] Update CHANGELOG.md with deprecations --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 202b5f4a41..cce7bf8104 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1409,6 +1409,11 @@ Deprecated names * In `Data.Vec.Properties`: ``` + take-distr-zipWith ↦ take-zipWith + take-distr-map ↦ take-map + drop-distr-zipWith ↦ drop-zipWith + drop-distr-map ↦ drop-map + updateAt-id-relative ↦ updateAt-id-local updateAt-compose-relative ↦ updateAt-∘-local updateAt-compose ↦ updateAt-∘