diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 18:09:36 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 18:09:36 +0200 |
| commit | cbda266091d45e564fc91462856e4f0571d18aca (patch) | |
| tree | 5a7ffb173076dc5f0bbe38b89f6ad9fbb2200647 /src/Data/Array | |
| parent | 952228e1b598f2a7e635f41e6ecd87e81145781e (diff) | |
Some more generators for tests
Diffstat (limited to 'src/Data/Array')
| -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 |