diff options
Diffstat (limited to 'src/Data/Array/Mixed')
| -rw-r--r-- | src/Data/Array/Mixed/Types.hs | 5 |
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 |