diff options
author | Mikolaj Konarski <mikolaj.konarski@gmail.com> | 2024-04-22 16:29:00 +0200 |
---|---|---|
committer | Mikolaj Konarski <mikolaj.konarski@gmail.com> | 2024-04-22 16:29:00 +0200 |
commit | 7156d267a25b01ccc615fcd0a197a5079e5acf3f (patch) | |
tree | 9646c71fdad5665d106858a9bfc2149f3ac1a384 | |
parent | c4598014eaac54018a6aad9621b8e667a0e84cf6 (diff) |
Add ToINat
-rw-r--r-- | src/Data/INat.hs | 7 |
1 files changed, 6 insertions, 1 deletions
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) |