diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 23:08:58 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 23:52:03 +0200 |
| commit | 67b62499a6d60fed9489f0371a8c841beb0c308f (patch) | |
| tree | b83d488760d2fcc6cf4be73c890824e8e6bc2480 /src/Data/Array/Nested/Shaped/Shape.hs | |
| parent | dec7d6c47fe9b783e1a98008a4efffb77df6f393 (diff) | |
Use lazilyConcat for listxAppend
Diffstat (limited to 'src/Data/Array/Nested/Shaped/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index 13596a7..fe55d1a 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -119,9 +119,9 @@ listsLast :: ListS (n : sh) i -> i listsLast (_ ::$ sh@(_ ::$ _)) = listsLast sh listsLast (n ::$ ZS) = n -listsAppend :: ListS sh i -> ListS sh' i -> ListS (sh ++ sh') i -listsAppend ZS idx' = idx' -listsAppend (i ::$ idx) idx' = i ::$ listsAppend idx idx' +listsAppend :: forall sh sh' i. ListS sh i -> ListS sh' i -> ListS (sh ++ sh') i +listsAppend = gcastWith (unsafeCoerceRefl :: MapJust (sh ++ sh') :~: MapJust sh ++ MapJust sh') $ + coerce (listxAppend @_ @_ @i) listsZip :: ListS sh i -> ListS sh j -> ListS sh (i, j) listsZip ZS ZS = ZS @@ -219,7 +219,7 @@ ixsCast ZIS = ZIS ixsCast (i :.$ idx) = i :.$ ixsCast idx ixsAppend :: forall sh sh' i. IxS sh i -> IxS sh' i -> IxS (sh ++ sh') i -ixsAppend = coerce (listsAppend @_ @i) +ixsAppend = coerce (listsAppend @_ @_ @i) ixsZip :: IxS sh i -> IxS sh j -> IxS sh (i, j) ixsZip ZIS ZIS = ZIS |