From 52fc156074f538409f5c382aa399a47357392ed0 Mon Sep 17 00:00:00 2001 From: SlayerOfTheBad Date: Thu, 20 Feb 2025 21:24:01 +0100 Subject: [PATCH 1/2] Migrate contrib:Data.Vect.Views.Extra to base:Data.Vect.Views This mirrors the structure of Data.List.Views, and is consistent with the location mentioned in TDDwI. --- .../Data/Vect/Views/Extra.idr => base/Data/Vect/Views.idr} | 4 ++-- libs/base/base.ipkg | 1 + libs/contrib/contrib.ipkg | 1 - tests/idris2/with/with011/WithImplicits.idr | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) rename libs/{contrib/Data/Vect/Views/Extra.idr => base/Data/Vect/Views.idr} (97%) diff --git a/libs/contrib/Data/Vect/Views/Extra.idr b/libs/base/Data/Vect/Views.idr similarity index 97% rename from libs/contrib/Data/Vect/Views/Extra.idr rename to libs/base/Data/Vect/Views.idr index 080cee41f6..4a4d8efe9a 100644 --- a/libs/contrib/Data/Vect/Views/Extra.idr +++ b/libs/base/Data/Vect/Views.idr @@ -1,5 +1,5 @@ -||| Additional views for Vect -module Data.Vect.Views.Extra +||| Views for Vect +module Data.Vect.Views import Control.WellFounded import Data.Vect diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 4b8d050883..0a466d04da 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -98,6 +98,7 @@ modules = Control.App, Data.Vect.AtIndex, Data.Vect.Elem, Data.Vect.Quantifiers, + Data.Vect.Views, Data.Void, Data.Zippable, diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 5454957a37..2dfb7abed9 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -94,7 +94,6 @@ modules = Control.ANSI, Data.Vect.Properties.Fin, Data.Vect.Extra, Data.Vect.Sort, - Data.Vect.Views.Extra, Debug.Buffer, diff --git a/tests/idris2/with/with011/WithImplicits.idr b/tests/idris2/with/with011/WithImplicits.idr index 9cf8dce303..499b3a966e 100644 --- a/tests/idris2/with/with011/WithImplicits.idr +++ b/tests/idris2/with/with011/WithImplicits.idr @@ -1,5 +1,5 @@ import Data.Vect -import Data.Vect.Views.Extra +import Data.Vect.Views mergeSort : Ord a => {n : _} -> Vect n a -> Vect n a mergeSort input with (splitRec input) From c03baaadcac6b8d8448177058c3d30ac29033693 Mon Sep 17 00:00:00 2001 From: SlayerOfTheBad Date: Thu, 20 Feb 2025 21:30:05 +0100 Subject: [PATCH 2/2] Update Changelog --- CHANGELOG_NEXT.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 0e22fb81ba..9eac3cb9ca 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -205,6 +205,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO #### Base +* `Data.Vect.Views.Extra` was moved from `contrib` to `base`. + * `Data.List.Lazy` was moved from `contrib` to `base`. * Added an `Interpolation` implementation for primitive decimal numeric types and `Nat`. @@ -287,6 +289,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO #### Contrib +* `Data.Vect.Views.Extra` was moved from `contrib` to `base`. + * `Data.List.Lazy` was moved from `contrib` to `base`. * Existing `System.Console.GetOpt` was extended to support errors during options