diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2024-05-15 13:49:53 +0200 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2024-05-15 13:58:05 +0200 |
| commit | e2c96efd486beeb7f690a468edec4e978c56f994 (patch) | |
| tree | 790091c87286cc527a06f5b9aaa5756511addd62 /src/Data/Array/Nested | |
| parent | bd11ee13d58c512f1a9cc0ef06b36c722653ff6f (diff) | |
Consistently n + 1
Diffstat (limited to 'src/Data/Array/Nested')
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs index 222247b..627e0d3 100644 --- a/src/Data/Array/Nested/Internal.hs +++ b/src/Data/Array/Nested/Internal.hs @@ -171,7 +171,7 @@ lemReplicateSucc = unsafeCoerce Refl lemAppLeft :: Proxy l -> a :~: b -> a ++ l :~: b ++ l lemAppLeft _ Refl = Refl -knownNatSucc :: KnownNat n => Dict KnownNat (1 + n) +knownNatSucc :: KnownNat n => Dict KnownNat (n + 1) knownNatSucc = Dict @@ -988,7 +988,7 @@ pattern ZIR = IxR ZR pattern (:.:) :: forall {n1} {i}. - forall n. (1 + n ~ n1) + forall n. (n + 1 ~ n1) => i -> IxR n i -> IxR n1 i pattern i :.: sh <- (unconsIxR -> Just (UnconsIxRRes sh i)) where i :.: IxR sh = IxR (i ::: sh) @@ -996,7 +996,7 @@ pattern i :.: sh <- (unconsIxR -> Just (UnconsIxRRes sh i)) infixr 3 :.: data UnconsIxRRes i n1 = - forall n. (1 + n ~ n1) => UnconsIxRRes (IxR n i) i + forall n. (n + 1 ~ n1) => UnconsIxRRes (IxR n i) i unconsIxR :: IxR n1 i -> Maybe (UnconsIxRRes i n1) unconsIxR (IxR (i ::: sh')) = Just (UnconsIxRRes (IxR sh') i) unconsIxR (IxR ZR) = Nothing @@ -1019,7 +1019,7 @@ pattern ZSR = ShR ZR pattern (:$:) :: forall {n1} {i}. - forall n. (1 + n ~ n1) + forall n. (n + 1 ~ n1) => i -> ShR n i -> ShR n1 i pattern i :$: sh <- (unconsShR -> Just (UnconsShRRes sh i)) where i :$: (ShR sh) = ShR (i ::: sh) @@ -1027,7 +1027,7 @@ pattern i :$: sh <- (unconsShR -> Just (UnconsShRRes sh i)) infixr 3 :$: data UnconsShRRes i n1 = - forall n. 1 + n ~ n1 => UnconsShRRes (ShR n i) i + forall n. n + 1 ~ n1 => UnconsShRRes (ShR n i) i unconsShR :: ShR n1 i -> Maybe (UnconsShRRes i n1) unconsShR (ShR (i ::: sh')) = Just (UnconsShRRes (ShR sh') i) unconsShR (ShR ZR) = Nothing @@ -1107,7 +1107,7 @@ rsumOuter1P (Ranked arr) $ arr rsumOuter1 :: forall n a. (Storable a, Num a, PrimElt a, KnownNat n) - => Ranked (1 + n) a -> Ranked n a + => Ranked (n + 1) a -> Ranked n a rsumOuter1 = coerce fromPrimitive . rsumOuter1P @n @a . coerce toPrimitive rtranspose :: forall n a. (KnownNat n, Elt a) => [Int] -> Ranked n a -> Ranked n a |