diff options
Diffstat (limited to 'src/Data/Array/Nested/Shaped')
| -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 |