From cbda266091d45e564fc91462856e4f0571d18aca Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Mon, 3 Jun 2024 18:09:36 +0200
Subject: Some more generators for tests

---
 src/Data/Array/Mixed/Types.hs | 5 ++++-
 1 file changed, 4 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 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
-- 
cgit v1.2.3-70-g09d2