diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-02 10:32:53 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-02 10:33:33 +0200 |
| commit | 31a603bb5d685306fe9561eac25c62b514c62be2 (patch) | |
| tree | 3a28f94bfa60eb215ae3dcd9329c405c9fa8ce82 /src/Data/Array/Nested/Shaped/Shape.hs | |
| parent | fc2a1370d67f12b50e3e5750d17aefd33bc3d8a3 (diff) | |
Rename TakeLen functions to TakeLenPerm; same for Drop
Diffstat (limited to 'src/Data/Array/Nested/Shaped/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index ef91c7b..f83a065 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -424,17 +424,17 @@ shsAppend = :: MapJust sh ++ MapJust sh' :~: MapJust (sh ++ sh')) $ coerce (shxAppend @_ @_ @Int) -shsTakeLen :: forall is sh. Perm is -> ShS sh -> ShS (TakeLen is sh) -shsTakeLen = +shsTakeLenPerm :: forall is sh. Perm is -> ShS sh -> ShS (TakeLen is sh) +shsTakeLenPerm = gcastWith (unsafeCoerceRefl :: TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)) $ - coerce shxTakeLen + coerce shxTakeLenPerm -shsDropLen :: forall is sh. Perm is -> ShS sh -> ShS (DropLen is sh) -shsDropLen = +shsDropLenPerm :: forall is sh. Perm is -> ShS sh -> ShS (DropLen is sh) +shsDropLenPerm = gcastWith (unsafeCoerceRefl :: DropLen is (MapJust sh) :~: MapJust (DropLen is sh)) $ - coerce shxDropLen + coerce shxDropLenPerm shsPermute :: forall is sh. Perm is -> ShS sh -> ShS (Permute is sh) shsPermute = @@ -455,7 +455,7 @@ shsPermutePrefix perm (ShS shx) | Refl <- lemTakeLenMapJust perm sh , Refl <- lemDropLenMapJust perm sh , Refl <- lemPermuteMapJust perm sh - , Refl <- lemMapJustApp (shsPermute perm (shsTakeLen perm sh)) (shsDropLen perm sh) -} + , Refl <- lemMapJustApp (shsPermute perm (shsTakeLenPerm perm sh)) (shsDropLenPerm perm sh) -} = gcastWith (unsafeCoerceRefl :: Permute is (TakeLen is (MapJust sh)) ++ DropLen is (MapJust sh) |