From 78d6c0640a3212d6a347c206c8b5fdb53bc0a6b9 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 13 Nov 2024 20:23:10 +0100 Subject: snatMinus --- src/Data/Array/Mixed/Types.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/Data/Array/Mixed') 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 @@ -78,6 +78,10 @@ snatPred snp1 = 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 -- cgit v1.2.3-70-g09d2