Simple usage example

1 files changed, 17 insertions, 0 deletions

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