From 7156d267a25b01ccc615fcd0a197a5079e5acf3f Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@gmail.com>
Date: Mon, 22 Apr 2024 16:29:00 +0200
Subject: Add ToINat

---
 src/Data/INat.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Data/INat.hs b/src/Data/INat.hs
index f7523ee..7a495ca 100644
--- a/src/Data/INat.hs
+++ b/src/Data/INat.hs
@@ -43,7 +43,7 @@ pattern SINat' <- (snatKnown -> Dict)
   where SINat' = inatSing
 
 -- | A 'KnownINat' dictionary is just a singleton natural, so we can create
--- evidence of 'KnownNat' given an 'SINat'.
+-- evidence of 'KnownINat' given an 'SINat'.
 snatKnown :: SINat n -> Dict KnownINat n
 snatKnown SZ = Dict
 snatKnown (SS n) | Dict <- snatKnown n = Dict
@@ -72,6 +72,11 @@ type family FromINat n where
   FromINat Z = 0
   FromINat (S n) = 1 + FromINat n
 
+-- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'.
+type family ToINat n where
+  ToINat 0 = Z
+  ToINat n = S (ToINat (n - 1))
+
 -- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits"
 -- 'G.Nat' is also known.
 knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n)
-- 
cgit v1.2.3-70-g09d2