diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-05 18:30:30 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-05 18:33:37 +0200 |
| commit | 574468a37a0e662c5d63d1cf3f8f876b11b4e332 (patch) | |
| tree | d6015b45903ad21b04533d0bef52cfd38fca5d01 /src/Data/Array/Nested/Shaped/Shape.hs | |
| parent | 84c0878bbae11dbcab0f5b342386a20f716d2397 (diff) | |
Tweak sized list type synonyms slightly
Diffstat (limited to 'src/Data/Array/Nested/Shaped/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index fe55d1a..bec2495 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -63,16 +63,16 @@ pattern (::$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> ListS sh i -> ListS sh1 i -pattern i ::$ sh <- (listsUncons -> Just (UnconsListSRes sh i)) - where i ::$ ListS sh = ListS (i ::% sh) +pattern i ::$ l <- (listsUncons -> Just (UnconsListSRes i l)) + where i ::$ ListS l = ListS (i ::% l) infixr 3 ::$ data UnconsListSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh i) i + forall n sh. (n : sh ~ sh1) => UnconsListSRes i (ListS sh i) listsUncons :: forall sh1 i. ListS sh1 i -> Maybe (UnconsListSRes i sh1) -listsUncons (ListS (x ::% sh')) | Refl <- lemMapJustHead (Proxy @sh1) - , Refl <- lemMapJustCons @sh1 Refl = - Just (UnconsListSRes (ListS sh') x) +listsUncons (ListS (i ::% l)) | Refl <- lemMapJustHead (Proxy @sh1) + , Refl <- lemMapJustCons @sh1 Refl = + Just (UnconsListSRes i (ListS l)) listsUncons (ListS _) = Nothing {-# COMPLETE ZS, (::$) #-} @@ -171,8 +171,8 @@ pattern (:.$) :: forall {sh1} {i}. forall n sh. (n : sh ~ sh1) => i -> IxS sh i -> IxS sh1 i -pattern i :.$ sh <- IxS (i ::$ (IxS -> sh)) - where i :.$ IxS sh = IxS (i ::$ sh) +pattern i :.$ l <- IxS (i ::$ (IxS -> l)) + where i :.$ IxS l = IxS (i ::$ l) infixr 3 :.$ {-# COMPLETE ZIS, (:.$) #-} @@ -289,8 +289,7 @@ infixr 3 :$$ data UnconsShSRes sh1 = forall n sh. (n : sh ~ sh1) => UnconsShSRes (SNat n) (ShS sh) shsUncons :: forall sh1. ShS sh1 -> Maybe (UnconsShSRes sh1) -shsUncons (ShS (SKnown x :$% sh')) - | Refl <- lemMapJustCons @sh1 Refl +shsUncons (ShS (SKnown x :$% sh')) | Refl <- lemMapJustCons @sh1 Refl = Just (UnconsShSRes x (ShS sh')) shsUncons (ShS _) = Nothing |