From ffa91484573a2c2be3f6ae2190c768e7a77e8b5c Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Wed, 3 Apr 2024 15:06:52 +0200
Subject: Simple usage example

---
 src/Data/Nat.hs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src/Data/Nat.hs')

diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index 5dacc8a..b154f67 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -44,6 +44,10 @@ unSNat :: SNat n -> Natural
 unSNat SZ = 0
 unSNat (SS n) = 1 + unSNat n
 
+-- | Convert an 'SNat' to an integer.
+unSNat' :: SNat n -> Int
+unSNat' = fromIntegral . unSNat
+
 -- | A 'KnownNat' dictionary is just a singleton natural, so we can create
 -- evidence of 'KnownNat' given an 'SNat'.
 snatKnown :: SNat n -> Dict KnownNat n
@@ -68,3 +72,16 @@ gknownNat (Proxy @n) = go (knownNat @n)
     go :: SNat m -> Dict G.KnownNat (GNat m)
     go SZ = Dict
     go (SS n) | Dict <- go n = Dict
+
+-- * Some type-level naturals
+
+type N0 = Z
+type N1 = S N0
+type N2 = S N1
+type N3 = S N2
+type N4 = S N3
+type N5 = S N4
+type N6 = S N5
+type N7 = S N6
+type N8 = S N7
+type N9 = S N8
-- 
cgit v1.2.3-70-g09d2