aboutsummaryrefslogtreecommitdiff
path: root/src/Data/Array/Nested
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Array/Nested')
-rw-r--r--src/Data/Array/Nested/Internal.hs12
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