diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-13 20:23:10 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-13 20:23:10 +0100 |
| commit | 78d6c0640a3212d6a347c206c8b5fdb53bc0a6b9 (patch) | |
| tree | 611078c4ffd92e63e3264a2456db395f24e797fa /src | |
| parent | bf4a469f369f1b8c6b1c2d7cc6907177405603f4 (diff) | |
snatMinus
Diffstat (limited to 'src')
| -rw-r--r-- | src/Data/Array/Mixed/Types.hs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Data/Array/Mixed/Types.hs b/src/Data/Array/Mixed/Types.hs index 8e90a88..13675d0 100644 --- a/src/Data/Array/Mixed/Types.hs +++ b/src/Data/Array/Mixed/Types.hs @@ -19,7 +19,7 @@ module Data.Array.Mixed.Types ( -- * Type-level naturals pattern SZ, pattern SS, fromSNat', sameNat', - snatPlus, snatMul, + snatPlus, snatMinus, snatMul, snatSucc, -- * Type-level lists @@ -79,6 +79,10 @@ snatPlus :: SNat n -> SNat m -> SNat (n + m) snatPlus n m = TN.withSomeSNat (TN.fromSNat n + TN.fromSNat m) Unsafe.Coerce.unsafeCoerce -- This should be a function in base +snatMinus :: SNat n -> SNat m -> SNat (n - m) +snatMinus n m = let res = TN.fromSNat n - TN.fromSNat m in res `seq` TN.withSomeSNat res Unsafe.Coerce.unsafeCoerce + +-- This should be a function in base snatMul :: SNat n -> SNat m -> SNat (n * m) snatMul n m = TN.withSomeSNat (TN.fromSNat n * TN.fromSNat m) Unsafe.Coerce.unsafeCoerce |