aboutsummaryrefslogtreecommitdiff
path: root/src/Data/Array
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Array')
-rw-r--r--src/Data/Array/Mixed/Types.hs5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Data/Array/Mixed/Types.hs b/src/Data/Array/Mixed/Types.hs
index 52201df..35e6fd3 100644
--- a/src/Data/Array/Mixed/Types.hs
+++ b/src/Data/Array/Mixed/Types.hs
@@ -18,7 +18,7 @@ module Data.Array.Mixed.Types (
-- * Type-level naturals
pattern SZ, pattern SS,
- fromSNat',
+ fromSNat', sameNat',
snatPlus, snatMul,
-- * Type-level lists
@@ -46,6 +46,9 @@ data Dict c a where
fromSNat' :: SNat n -> Int
fromSNat' = fromIntegral . fromSNat
+sameNat' :: SNat n -> SNat m -> Maybe (n :~: m)
+sameNat' n@SNat m@SNat = sameNat n m
+
pattern SZ :: () => (n ~ 0) => SNat n
pattern SZ <- ((\sn -> testEquality sn (SNat @0)) -> Just Refl)
where SZ = SNat