summaryrefslogtreecommitdiff
path: root/src/Data.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data.hs')
-rw-r--r--src/Data.hs4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index 1304a5f..60afdd0 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -101,6 +101,10 @@ type family n + m where
Z + m = m
S n + m = S (n + m)
+type family n - m where
+ n - Z = n
+ S n - S m = n - m
+
snatAdd :: SNat n -> SNat m -> SNat (n + m)
snatAdd SZ m = m
snatAdd (SS n) m = SS (snatAdd n m)