From 7156d267a25b01ccc615fcd0a197a5079e5acf3f Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski 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